75 val (ct,_) = the (rewrite_set_inst thy' false |
75 val (ct,_) = the (rewrite_set_inst thy' false |
76 [("bdv","x::real")] rls ct); |
76 [("bdv","x::real")] rls ct); |
77 (*"x = (0 + -1 * -36) // -15"*) |
77 (*"x = (0 + -1 * -36) // -15"*) |
78 val rls = ("Test_simplify"); |
78 val rls = ("Test_simplify"); |
79 val (ct,_) = the (rewrite_set thy' false rls ct); |
79 val (ct,_) = the (rewrite_set thy' false rls ct); |
80 if ct<>"x = -12 / 5"then raise error "new behaviour in testexample"else (); |
80 if ct<>"x = -12 / 5"then error "new behaviour in testexample"else (); |
81 |
81 |
82 (* |
82 (* |
83 val ct = "x = (-12) / 5" : cterm' |
83 val ct = "x = (-12) / 5" : cterm' |
84 > asm; |
84 > asm; |
85 val it = |
85 val it = |
201 val (t,_) = the (rewrite_set_inst_ thy false subst rls t); |
201 val (t,_) = the (rewrite_set_inst_ thy false subst rls t); |
202 val rls = Test_simplify; |
202 val rls = Test_simplify; |
203 val (t,_) = the (rewrite_set_ thy false rls t); |
203 val (t,_) = the (rewrite_set_ thy false rls t); |
204 val t' = term2str t; |
204 val t' = term2str t; |
205 if t' = "x = 4" then () |
205 if t' = "x = 4" then () |
206 else raise error "root-equ.sml: new behav. in rewrite_ x+4"; |
206 else error "root-equ.sml: new behav. in rewrite_ x+4"; |
207 |
207 |
208 " _________________ rewrite x=4_________________ "; |
208 " _________________ rewrite x=4_________________ "; |
209 " _________________ rewrite x=4_________________ "; |
209 " _________________ rewrite x=4_________________ "; |
210 " _________________ rewrite x=4_________________ "; |
210 " _________________ rewrite x=4_________________ "; |
211 (* |
211 (* |
247 val (ct,_) = the (rewrite_set_inst thy' false |
247 val (ct,_) = the (rewrite_set_inst thy' false |
248 [("bdv","x")] rls ct); |
248 [("bdv","x")] rls ct); |
249 "x = 0 + -1 * -4"; |
249 "x = 0 + -1 * -4"; |
250 (*11*)val rls = "Test_simplify"; |
250 (*11*)val rls = "Test_simplify"; |
251 val (ct,_) = the (rewrite_set thy' false rls ct); |
251 val (ct,_) = the (rewrite_set thy' false rls ct); |
252 if ct="x = 4" then () else raise error "new behaviour in test-example"; |
252 if ct="x = 4" then () else error "new behaviour in test-example"; |
253 |
253 |
254 |
254 |
255 |
255 |
256 |
256 |
257 " _________________ rewrite + cappend _________________ "; |
257 " _________________ rewrite + cappend _________________ "; |
627 "--- 1<> ---"; |
627 "--- 1<> ---"; |
628 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]); |
628 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]); |
629 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
629 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
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 raise 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_ptree 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=============================================================="); |