equal
deleted
inserted
replaced
202 then (r, imp_intr_tac i THEN rotate_tac ~1 i) |
202 then (r, imp_intr_tac i THEN rotate_tac ~1 i) |
203 else (*leave affected hyps at end*) |
203 else (*leave affected hyps at end*) |
204 (r+1, imp_intr_tac i) |
204 (r+1, imp_intr_tac i) |
205 in |
205 in |
206 case Seq.pull(tac st) of |
206 case Seq.pull(tac st) of |
207 None => Seq.single(st) |
207 NONE => Seq.single(st) |
208 | Some(st',_) => imptac (r',hyps) st' |
208 | SOME(st',_) => imptac (r',hyps) st' |
209 end handle _ => error "?? in blast_hyp_subst_tac" |
209 end handle _ => error "?? in blast_hyp_subst_tac" |
210 in imptac (0, rev hyps) end; |
210 in imptac (0, rev hyps) end; |
211 |
211 |
212 |
212 |
213 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => |
213 fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) => |