equal
deleted
inserted
replaced
186 |
186 |
187 fun cont_tac i = resolve_tac cont_lemmas2 i; |
187 fun cont_tac i = resolve_tac cont_lemmas2 i; |
188 fun cont_tacR i = REPEAT (cont_tac i); |
188 fun cont_tacR i = REPEAT (cont_tac i); |
189 |
189 |
190 local val flift1_def = thm "flift1_def" |
190 local val flift1_def = thm "flift1_def" |
191 in fun cont_tacRs i = |
191 in fun cont_tacRs ss i = |
192 simp_tac (simpset()) i THEN |
192 simp_tac ss i THEN |
193 REPEAT (cont_tac i) |
193 REPEAT (cont_tac i) |
194 end; |
194 end; |
195 *} |
195 *} |
196 |
196 |
197 end |
197 end |