235 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
235 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
236 if f = Form' |
236 if f = Form' |
237 (FormKF |
237 (FormKF |
238 (~1,EdUndef,1,Nundef, |
238 (~1,EdUndef,1,Nundef, |
239 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)")) |
239 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)")) |
240 then () else raise error "behaviour in root-expl. Free_Solve changed"; |
240 then () else error "behaviour in root-expl. Free_Solve changed"; |
241 writeln (pr_ptree pr_short pt); |
241 writeln (pr_ptree pr_short pt); |
242 ---------------------------------meNEW raises exception with not-locatable*) |
242 ---------------------------------meNEW raises exception with not-locatable*) |
243 |
243 |
244 |
244 |
245 val d = e_rls; |
245 val d = e_rls; |
315 val ((pt,_),_) = get_calc 1; |
315 val ((pt,_),_) = get_calc 1; |
316 show_pt pt; |
316 show_pt pt; |
317 |
317 |
318 val tacs = sel_rules pt ([],Pbl); |
318 val tacs = sel_rules pt ([],Pbl); |
319 if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then () |
319 if tacs = [Apply_Method ["Test", "squ-equ-test-subpbl1"]] then () |
320 else raise error "script.sml: diff.behav. in sel_rules ([],Pbl)"; |
320 else error "script.sml: diff.behav. in sel_rules ([],Pbl)"; |
321 |
321 |
322 val tacs = sel_rules pt ([1],Res); |
322 val tacs = sel_rules pt ([1],Res); |
323 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", |
323 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", |
324 Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]), |
324 Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]), |
325 Check_elementwise "Assumptions"] then () |
325 Check_elementwise "Assumptions"] then () |
326 else raise error "script.sml: diff.behav. in sel_rules ([1],Res)"; |
326 else error "script.sml: diff.behav. in sel_rules ([1],Res)"; |
327 |
327 |
328 val tacs = sel_rules pt ([3],Pbl); |
328 val tacs = sel_rules pt ([3],Pbl); |
329 if tacs = [Apply_Method ["Test", "solve_linear"]] then () |
329 if tacs = [Apply_Method ["Test", "solve_linear"]] then () |
330 else raise error "script.sml: diff.behav. in sel_rules ([3],Pbl)"; |
330 else error "script.sml: diff.behav. in sel_rules ([3],Pbl)"; |
331 |
331 |
332 val tacs = sel_rules pt ([3,1],Res); |
332 val tacs = sel_rules pt ([3,1],Res); |
333 if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), |
333 if tacs = [Rewrite_Set_Inst (["(bdv, x)"], "isolate_bdv"), |
334 Rewrite_Set "Test_simplify"] then () |
334 Rewrite_Set "Test_simplify"] then () |
335 else raise error "script.sml: diff.behav. in sel_rules ([3,1],Res)"; |
335 else error "script.sml: diff.behav. in sel_rules ([3,1],Res)"; |
336 |
336 |
337 val tacs = sel_rules pt ([3],Res); |
337 val tacs = sel_rules pt ([3],Res); |
338 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", |
338 if tacs = [Rewrite_Set "norm_equation", Rewrite_Set "Test_simplify", |
339 Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]), |
339 Subproblem ("Test.thy", ["linear", "univariate", "equation", "test"]), |
340 Check_elementwise "Assumptions"] then () |
340 Check_elementwise "Assumptions"] then () |
341 else raise error "script.sml: diff.behav. in sel_rules ([3],Res)"; |
341 else error "script.sml: diff.behav. in sel_rules ([3],Res)"; |
342 |
342 |
343 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str]; |
343 val tacs = (sel_rules pt ([],Res)) handle PTREE str => [Tac str]; |
344 if tacs = [Tac "no tactics applicable at the end of a calculation"] then () |
344 if tacs = [Tac "no tactics applicable at the end of a calculation"] then () |
345 else raise error "script.sml: diff.behav. in sel_rules ([],Res)"; |
345 else error "script.sml: diff.behav. in sel_rules ([],Res)"; |