250 \(While (contains_root e_e) Do \ |
250 \(While (contains_root e_e) Do \ |
251 \((Try (Repeat (Rewrite rroot_square_inv))) #> \ |
251 \((Try (Repeat (Rewrite rroot_square_inv))) #> \ |
252 \ (Try (Repeat (Rewrite square_equation_left))) #> \ |
252 \ (Try (Repeat (Rewrite square_equation_left))) #> \ |
253 \ (Try (Repeat (Rewrite radd_0)))))\ |
253 \ (Try (Repeat (Rewrite radd_0)))))\ |
254 \ e_e "); |
254 \ e_e "); |
255 TermC.atomty sc; |
255 TermC.atom_trace_detail @{context} sc; |
256 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"], |
256 val (dI',pI',mI') = ("Test",["sqroot-test", "univariate", "equation", "test"], |
257 ["Test", "sqrt-equ-test"]); |
257 ["Test", "sqrt-equ-test"]); |
258 val c = []; |
258 val c = []; |
259 val (p,_,_,_,_,pt) = Test_Code.init_calc @{context} [([], (dI',pI',mI')))]; |
259 val (p,_,_,_,_,pt) = Test_Code.init_calc @{context} [([], (dI',pI',mI')))]; |
260 val nxt = ("Specify_Theory",Specify_Theory "Test"); |
260 val nxt = ("Specify_Theory",Specify_Theory "Test"); |