equal
deleted
inserted
replaced
262 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"]; |
262 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"]; |
263 val oris = prep_ori ctl thy |
263 val oris = prep_ori ctl thy |
264 ((#ppc o get_pbt) |
264 ((#ppc o get_pbt) |
265 ["sqroot-test","univariate","equation","test"]); |
265 ["sqroot-test","univariate","equation","test"]); |
266 val loc = e_istate; |
266 val loc = e_istate; |
267 val (pt,pos) = (e_ptree,[]); |
267 val (pt,pos) = (e_ctree,[]); |
268 val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term); |
268 val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term); |
269 val pt = update_branch pt [] TransitiveB; |
269 val pt = update_branch pt [] TransitiveB; |
270 (* |
270 (* |
271 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt []))); |
271 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt []))); |
272 *) |
272 *) |
365 |
365 |
366 val pos = lev_up pos; |
366 val pos = lev_up pos; |
367 val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete; |
367 val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete; |
368 get_assumptions_ pt ([],Res); |
368 get_assumptions_ pt ([],Res); |
369 |
369 |
370 writeln (pr_ptree pr_short pt); |
370 writeln (pr_ctree pr_short pt); |
371 (* aus src.24-11-99: |
371 (* aus src.24-11-99: |
372 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0) |
372 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0) |
373 1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
373 1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
374 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
374 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
375 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2 |
375 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2 |
490 (* 5.4.00.: --- |
490 (* 5.4.00.: --- |
491 get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt; |
491 get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt; |
492 val (p,_,f,nxt,_,pt)= |
492 val (p,_,f,nxt,_,pt)= |
493 me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt; |
493 me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt; |
494 --- *) |
494 --- *) |
495 writeln (pr_ptree pr_short pt); |
495 writeln (pr_ctree pr_short pt); |
496 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*; |
496 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*; |
497 *) |
497 *) |
498 |
498 |
499 |
499 |
500 " _________________ me + tacs input _________________ "; |
500 " _________________ me + tacs input _________________ "; |
630 (* val nxt = ("End_Proof'",End_Proof');*) |
630 (* val nxt = ("End_Proof'",End_Proof');*) |
631 if f <> (Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
631 if f <> (Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
632 then error "root-equ.sml: diff.behav. in me + tacs input" |
632 then error "root-equ.sml: diff.behav. in me + tacs input" |
633 else (); |
633 else (); |
634 |
634 |
635 writeln (pr_ptree pr_short pt); |
635 writeln (pr_ctree pr_short pt); |
636 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^ |
636 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^ |
637 "\n=============================================================="); |
637 "\n=============================================================="); |
638 |
638 |