author  paulson 
Thu, 06 Nov 1997 10:29:37 +0100  
changeset 4179  cc4b6791d5dc 
parent 3537  79ac9b475621 
child 4223  f60e3d2c81d3 
permissions  rwrr 
0  1 
(* Title: Provers/hypsubst 
2 
ID: $Id$ 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

3 
Authors: Martin D Coen, Tobias Nipkow and Lawrence C Paulson 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

4 
Copyright 1995 University of Cambridge 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

5 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

6 
Tactic to substitute using the assumption x=t in the rest of the subgoal, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

7 
and to delete that assumption. Original version due to Martin Coen. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

8 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

9 
This version uses the simplifier, and requires it to be already present. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

10 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

11 
Test data: 
0  12 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

13 
goal thy "!!x.[ Q(x,y,z); y=x; a=x; z=y; P(y) ] ==> P(z)"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

14 
goal thy "!!x.[ Q(x,y,z); z=f(x); x=z ] ==> P(z)"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

15 
goal thy "!!y. [ ?x=y; P(?x) ] ==> y = a"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

16 
goal thy "!!z. [ ?x=y; P(?x) ] ==> y = a"; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

17 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

18 
by (hyp_subst_tac 1); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

19 
by (bound_hyp_subst_tac 1); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

20 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

21 
Here hyp_subst_tac goes wrong; harder still to prove P(f(f(a))) & P(f(a)) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

22 
goal thy "P(a) > (EX y. a=y > P(f(a)))"; 
0  23 
*) 
24 

25 
signature HYPSUBST_DATA = 

26 
sig 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

27 
structure Simplifier : SIMPLIFIER 
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

28 
val dest_eq : term > term*term*typ 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

29 
val eq_reflection : thm (* a=b ==> a==b *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

30 
val imp_intr : thm (* (P ==> Q) ==> P>Q *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

31 
val rev_mp : thm (* [ P; P>Q ] ==> Q *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

32 
val subst : thm (* [ a=b; P(a) ] ==> P(b) *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

33 
val sym : thm (* a=b ==> b=a *) 
0  34 
end; 
35 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

36 

0  37 
signature HYPSUBST = 
38 
sig 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

39 
val bound_hyp_subst_tac : int > tactic 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

40 
val hyp_subst_tac : int > tactic 
0  41 
(*exported purely for debugging purposes*) 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

42 
val gen_hyp_subst_tac : bool > int > tactic 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

43 
val vars_gen_hyp_subst_tac : bool > int > tactic 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

44 
val eq_var : bool > bool > term > int * bool 
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

45 
val inspect_pair : bool > bool > term * term * typ > bool 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

46 
val mk_eqs : thm > thm list 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

47 
val thin_leading_eqs_tac : bool > int > int > tactic 
0  48 
end; 
49 

2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

50 

3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

51 

0  52 
functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST = 
53 
struct 

54 

55 
local open Data in 

56 

57 
exception EQ_VAR; 

58 

2174  59 
fun loose (i,t) = 0 mem_int add_loose_bnos(t,i,[]); 
0  60 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

61 
local val odot = ord"." 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

62 
in 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

63 
(*Simplifier turns Bound variables to dotted Free variables: 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

64 
change it back (any Bound variable will do) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

65 
*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

66 
fun contract t = 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

67 
case Pattern.eta_contract_atom t of 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

68 
Free(a,T) => if (ord a = odot) then Bound 0 else Free(a,T) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

69 
 t' => t' 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

70 
end; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

71 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

72 
fun has_vars t = maxidx_of_term t <> ~1; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

73 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

74 
(*If novars then we forbid Vars in the equality. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

75 
If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

76 
When can we safely delete the equality? 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

77 
Not if it equates two constants; consider 0=1. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

78 
Not if it resembles x=t[x], since substitution does not eliminate x. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

79 
Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

80 
Not if it involves a variable free in the premises, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

81 
but we can't check for this  hence bnd and bound_hyp_subst_tac 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

82 
Prefer to eliminate Bound variables if possible. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

83 
Result: true = use as is, false = reorient first *) 
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

84 
fun inspect_pair bnd novars (t,u,T) = 
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

85 
if novars andalso maxidx_of_typ T <> ~1 
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

86 
then raise Match (*variables in the type!*) 
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
3537
diff
changeset

87 
else 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

88 
case (contract t, contract u) of 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

89 
(Bound i, _) => if loose(i,u) orelse novars andalso has_vars u 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

90 
then raise Match 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

91 
else true (*eliminates t*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

92 
 (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

93 
then raise Match 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

94 
else false (*eliminates u*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

95 
 (Free _, _) => if bnd orelse Logic.occs(t,u) orelse 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

96 
novars andalso has_vars u 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

97 
then raise Match 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

98 
else true (*eliminates t*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

99 
 (_, Free _) => if bnd orelse Logic.occs(u,t) orelse 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

100 
novars andalso has_vars t 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

101 
then raise Match 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

102 
else false (*eliminates u*) 
0  103 
 _ => raise Match; 
104 

680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

105 
(*Locates a substitutable variable on the left (resp. right) of an equality 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

106 
assumption. Returns the number of intervening assumptions. *) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

107 
fun eq_var bnd novars = 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

108 
let fun eq_var_aux k (Const("all",_) $ Abs(_,_,t)) = eq_var_aux k t 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

109 
 eq_var_aux k (Const("==>",_) $ A $ B) = 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

110 
((k, inspect_pair bnd novars (dest_eq A)) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

111 
(*Exception comes from inspect_pair or dest_eq*) 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

112 
handle Match => eq_var_aux (k+1) B) 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

113 
 eq_var_aux k _ = raise EQ_VAR 
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

114 
in eq_var_aux 0 end; 
0  115 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

116 
(*We do not try to delete ALL equality assumptions at once. But 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

117 
it is easy to handle several consecutive equality assumptions in a row. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

118 
Note that we have to inspect the proof state after doing the rewriting, 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

119 
since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

120 
must NOT be deleted. Tactic must rotate or delete m assumptions. 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

121 
*) 
3537  122 
fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

123 
let fun count [] = 0 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

124 
 count (A::Bs) = ((inspect_pair bnd true (dest_eq A); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

125 
1 + count Bs) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

126 
handle Match => 0) 
2143  127 
val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) 
2722
3e07c20b967c
Now uses rotate_tac and eta_contract_atom for greater speed
paulson
parents:
2174
diff
changeset

128 
in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (mj) i 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

129 
end); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

130 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

131 
(*For the simpset. Adds ALL suitable equalities, even if not first! 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

132 
No vars are allowed here, as simpsets are built from metaassumptions*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

133 
fun mk_eqs th = 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

134 
[ if inspect_pair false false (Data.dest_eq (#prop (rep_thm th))) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

135 
then th RS Data.eq_reflection 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

136 
else symmetric(th RS Data.eq_reflection) (*reorient*) ] 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

137 
handle Match => []; (*Exception comes from inspect_pair or dest_eq*) 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

138 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

139 
local open Simplifier 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

140 
in 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

141 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

142 
val hyp_subst_ss = empty_ss setmksimps mk_eqs 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

143 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

144 
(*Select a suitable equality assumption and substitute throughout the subgoal 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

145 
Replaces only Bound variables if bnd is true*) 
3537  146 
fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => 
147 
let val n = length(Logic.strip_assums_hyp Bi)  1 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

148 
val (k,_) = eq_var bnd true Bi 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

149 
in 
3537  150 
DETERM (EVERY [rotate_tac k i, 
151 
asm_full_simp_tac hyp_subst_ss i, 

152 
etac thin_rl i, 

153 
thin_leading_eqs_tac bnd (nk) i]) 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

154 
end 
3537  155 
handle THM _ => no_tac  EQ_VAR => no_tac); 
1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

156 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

157 
end; 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

158 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

159 
val ssubst = standard (sym RS subst); 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

160 

5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

161 
(*Old version of the tactic above  slower but the only way 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

162 
to handle equalities containing Vars.*) 
3537  163 
fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => 
164 
let val n = length(Logic.strip_assums_hyp Bi)  1 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

165 
val (k,symopt) = eq_var bnd false Bi 
680
f9e24455bbd1
Provers/hypsubst: greatly simplified! No longer simulates a
lcp
parents:
646
diff
changeset

166 
in 
3537  167 
DETERM 
168 
(EVERY [REPEAT_DETERM_N k (etac rev_mp i), 

169 
etac revcut_rl i, 

170 
REPEAT_DETERM_N (nk) (etac rev_mp i), 

171 
etac (if symopt then ssubst else subst) i, 

172 
REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) 

0  173 
end 
3537  174 
handle THM _ => no_tac  EQ_VAR => no_tac); 
0  175 

176 
(*Substitutes for Free or Bound variables*) 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

177 
val hyp_subst_tac = 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

178 
gen_hyp_subst_tac false ORELSE' vars_gen_hyp_subst_tac false; 
0  179 

180 
(*Substitutes for Bound variables only  this is always safe*) 

1011
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

181 
val bound_hyp_subst_tac = 
5c9654e2e3de
Recoded with help from Toby to use rewriting instead of the
lcp
parents:
704
diff
changeset

182 
gen_hyp_subst_tac true ORELSE' vars_gen_hyp_subst_tac true; 
0  183 

184 
end 

185 
end; 

186 