449 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) |
449 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs) |
450 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), |
450 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss), |
451 thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) |
451 thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) |
452 end |
452 end |
453 | NONE => if more |
453 | NONE => if more |
454 then rew((lhs_net_tac anet i THEN assume_tac i) thm, |
454 then rew((lhs_net_tac anet i THEN atac i) thm, |
455 thm,ss,anet,ats,cs,false) |
455 thm,ss,anet,ats,cs,false) |
456 else (ss,thm,anet,ats,cs); |
456 else (ss,thm,anet,ats,cs); |
457 |
457 |
458 fun try_true(thm,ss,anet,ats,cs) = |
458 fun try_true(thm,ss,anet,ats,cs) = |
459 case Seq.pull(auto_tac i thm) of |
459 case Seq.pull(auto_tac i thm) of |