equal
deleted
inserted
replaced
354 |
354 |
355 val pos = lev_up pos; |
355 val pos = lev_up pos; |
356 val (pt,pos) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete; |
356 val (pt,pos) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete; |
357 Ctree.get_assumptions pt ([],Res); |
357 Ctree.get_assumptions pt ([],Res); |
358 |
358 |
359 writeln (pr_ctree pr_short pt); |
359 writeln (pr_ctree ctxt pr_short pt); |
360 (* aus src.24-11-99: |
360 (* aus src.24-11-99: |
361 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0) |
361 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0) |
362 1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
362 1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
363 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
363 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
364 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) \<up> 2 |
364 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) \<up> 2 |
476 (* 5.4.00.: --- |
476 (* 5.4.00.: --- |
477 get_form ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) pt; |
477 get_form ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) pt; |
478 val (p,_,f,nxt,_,pt)= |
478 val (p,_,f,nxt,_,pt)= |
479 me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt; |
479 me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt; |
480 --- *) |
480 --- *) |
481 writeln (pr_ctree pr_short pt); |
481 writeln (pr_ctree ctxt pr_short pt); |
482 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*; |
482 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*; |
483 *) |
483 *) |
484 |
484 |
485 |
485 |
486 " _________________ me + tacs input _________________ "; |
486 " _________________ me + tacs input _________________ "; |
612 (* val nxt = ("End_Proof'",End_Proof');*) |
612 (* val nxt = ("End_Proof'",End_Proof');*) |
613 if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
613 if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
614 then error "root-equ.sml: diff.behav. in me + tacs input" |
614 then error "root-equ.sml: diff.behav. in me + tacs input" |
615 else (); |
615 else (); |
616 |
616 |
617 writeln (pr_ctree pr_short pt); |
617 writeln (pr_ctree ctxt pr_short pt); |
618 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^ |
618 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^ |
619 "\n=============================================================="); |
619 "\n=============================================================="); |
620 |
620 |