617 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
617 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
618 "--- 1<> ---"; |
618 "--- 1<> ---"; |
619 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]); |
619 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]); |
620 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
620 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
621 (* val nxt = ("End_Proof'",End_Proof');*) |
621 (* val nxt = ("End_Proof'",End_Proof');*) |
622 if f <> (Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
622 if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
623 then error "root-equ.sml: diff.behav. in me + tacs input" |
623 then error "root-equ.sml: diff.behav. in me + tacs input" |
624 else (); |
624 else (); |
625 |
625 |
626 writeln (pr_ctree pr_short pt); |
626 writeln (pr_ctree pr_short pt); |
627 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^ |
627 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^ |