9 "----------- setup presentation innsbruck ------------------------"; |
10 "----------- setup presentation innsbruck ------------------------"; |
10 "-----------------------------------------------------------------"; |
11 "-----------------------------------------------------------------"; |
11 "-----------------------------------------------------------------"; |
12 "-----------------------------------------------------------------"; |
12 "-----------------------------------------------------------------"; |
13 "-----------------------------------------------------------------"; |
13 |
14 |
14 (*=== inhibit exn ?============================================================= |
15 val thy = @{theory "LogExp"}; |
15 val thy = LogExp.thy; |
|
16 |
16 |
17 "----------- setup presentation innsbruck ------------------------"; |
17 "----------- setup presentation innsbruck ------------------------"; |
18 "----------- setup presentation innsbruck ------------------------"; |
18 "----------- setup presentation innsbruck ------------------------"; |
19 "----------- setup presentation innsbruck ------------------------"; |
19 "----------- setup presentation innsbruck ------------------------"; |
20 (* |
20 (* |
24 |
24 |
25 equality_power; |
25 equality_power; |
26 exp_invers_log; |
26 exp_invers_log; |
27 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac") works ? |
27 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac") works ? |
28 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"] |
28 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"] |
29 ["equation","test"]; |
29 ["equation","test"]; *) |
30 *) |
30 *) |
31 |
31 |
32 val t = str2term "(2 log x)"; |
32 val t = str2term "(2 log x)"; |
33 val t = str2term "(2 log x) = 3"; |
33 val t = str2term "(2 log x) = 3"; |
34 val t = str2term "matches ((?a log x) = ?b) ((2 log x) = 3)"; |
34 val t = str2term "matches ((?a log x) = ?b) ((2 log x) = 3)"; |
38 val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"]; |
38 val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"]; |
39 val (dI',pI',mI') = |
39 val (dI',pI',mI') = |
40 ("Isac",["logarithmic","univariate","equation","test"], |
40 ("Isac",["logarithmic","univariate","equation","test"], |
41 ["Test","solve_log"]); |
41 ["Test","solve_log"]); |
42 val p = e_pos'; val c = []; |
42 val p = e_pos'; val c = []; |
|
43 (*============ inhibit exn 110726 ============================================== |
43 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
44 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
44 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
45 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
45 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
46 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
46 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
47 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
47 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
48 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
56 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
57 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
57 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
58 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
58 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
59 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
59 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
60 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
60 show_pt pt; |
61 show_pt pt; |
|
62 ============ inhibit exn 110726 ==============================================*) |
61 |
63 |
62 *-------------------------------------------------------------------*) |
|
63 ===== inhibit exn ?===========================================================*) |
|