297 case ts of |
297 case ts of |
298 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end |
298 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end |
299 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac; |
299 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac; |
300 |
300 |
301 "~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''') |
301 "~~~~~ from fun me \<longrightarrow>toplevel , return:"; val (p''''',_,f,nxt''''',_,pt''''') |
302 = (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *), |
302 = (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *), |
303 tac, Celem.Sundef, pt); |
303 tac, Celem.Sundef, pt); |
304 (*\--------- step into 2. Check_Postcond -----------------------------------------------------/*) |
304 (*\--------- step into 2. Check_Postcond -----------------------------------------------------/*) |
305 |
305 |
306 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*) |
306 (*[4], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>IDLE LEGACY: Check_elementwise "Assumptions"*) |
307 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*) |
307 (*[], Res*)val (p,_,f,nxt,_,pt) = me nxt''''' p''''' [] pt''''';(*\<rightarrow>End_Proof'*) |