|
jan@42461
|
1 |
|
|
jan@42443
|
2 |
|
|
jan@42443
|
3 |
theory example_1 imports Isac
|
|
jan@42443
|
4 |
begin
|
|
jan@42443
|
5 |
|
|
jan@42444
|
6 |
section{*Equation Solving*}
|
|
jan@42444
|
7 |
text{*Setup equation, Calc Tree,\ldots*}
|
|
jan@42444
|
8 |
|
|
jan@42443
|
9 |
ML {*
|
|
jan@42461
|
10 |
val expr = ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",
|
|
jan@42461
|
11 |
"solveFor z", "solutions L"];
|
|
jan@42443
|
12 |
val (dI',pI',mI') =
|
|
jan@42443
|
13 |
("Isac",
|
|
jan@42443
|
14 |
["abcFormula","degree_2","polynomial","univariate","equation"],
|
|
jan@42443
|
15 |
["no_met"]);
|
|
jan@42443
|
16 |
*}
|
|
jan@42444
|
17 |
|
|
jan@42461
|
18 |
text{*Step through the Calculation*}
|
|
jan@42444
|
19 |
|
|
jan@42443
|
20 |
ML {*
|
|
jan@42443
|
21 |
val (p,_,f,nxt,_,pt) = CalcTreeTEST [(expr, (dI',pI',mI'))];
|
|
jan@42443
|
22 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
23 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
24 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
25 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
26 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
27 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
28 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
29 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
30 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
31 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
32 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
33 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
34 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
35 |
val (p,_,f,nxt,_,pt) = me nxt p [] pt;
|
|
jan@42443
|
36 |
*}
|
|
jan@42443
|
37 |
|
|
jan@42443
|
38 |
ML{*
|
|
jan@42443
|
39 |
f2str f;
|
|
jan@42443
|
40 |
show_pt pt;
|
|
jan@42443
|
41 |
*}
|
|
jan@42443
|
42 |
|
|
jan@42443
|
43 |
end
|