1 (* use"systest/auto-inform.sml"; |
1 (* use"systest/auto-inform.sml"; |
2 use"auto-inform.sml"; |
2 use"auto-inform.sml"; |
3 *) |
3 *) |
4 |
4 |
5 "autoCalculate"; |
5 "autoCalculate"; |
6 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
6 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
7 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
7 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
8 "--------- maximum-example: complete_metitms ---------------------"; |
8 "--------- maximum-example: complete_metitms ---------------------"; |
9 "--------- maximum-example: complete_mod -------------------------"; |
9 "--------- maximum-example: complete_mod -------------------------"; |
10 "appendForm with miniscript with mini-subpbl:"; |
10 "appendForm with miniscript with mini-subpbl:"; |
298 |
298 |
299 |
299 |
300 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
300 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
301 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
301 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
302 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
302 "--------- appendFormula: on Frm + equ_nrls ----------------------"; |
303 (**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**) |
|
304 states:=[]; |
303 states:=[]; |
305 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], |
304 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"], |
306 ("Test.thy", |
305 ("Test.thy", |
307 ["sqroot-test","univariate","equation","test"], |
306 ["sqroot-test","univariate","equation","test"], |
308 ["Test","squ-equ-test-subpbl1"]))]; |
307 ["Test","squ-equ-test-subpbl1"]))]; |
311 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
310 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*); |
312 |
311 |
313 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1); |
312 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1); |
314 |
313 |
315 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); |
314 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*); |
316 >>>>>>> 1.8 |
|
317 |
315 |
318 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm); |
316 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm); |
319 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res); |
317 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res); |
320 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res); |
318 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res); |
321 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res); |
319 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res); |