|
1 (* testexamples for LogExp, logarithms and exponential functions and terms |
|
2 |
|
3 use"../smltest/IsacKnowledge/logexp.sml"; |
|
4 *) |
|
5 |
|
6 val thy = LogExp.thy; |
|
7 "-----------------------------------------------------------------"; |
|
8 "table of contents -----------------------------------------------"; |
|
9 "-----------------------------------------------------------------"; |
|
10 "----------- setup presentation innsbruck ------------------------"; |
|
11 "-----------------------------------------------------------------"; |
|
12 "-----------------------------------------------------------------"; |
|
13 "-----------------------------------------------------------------"; |
|
14 |
|
15 |
|
16 "----------- setup presentation innsbruck ------------------------"; |
|
17 "----------- setup presentation innsbruck ------------------------"; |
|
18 "----------- setup presentation innsbruck ------------------------"; |
|
19 (* |
|
20 NOT INCLUDED IN ROOT.ML and RTEST-root.sml, since the pbl and met |
|
21 defined in IsacKnowledge/Test.ML are out-commented |
|
22 in order to allow for demonstration of authoring ! |
|
23 |
|
24 equality_power; |
|
25 exp_invers_log; |
|
26 (* WN071203 ???... wrong thy ?!? because parsing with Isac.thy works ? |
|
27 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"] |
|
28 ["equation","test"]; |
|
29 *) |
|
30 |
|
31 val t = str2term "(2 log x)"; |
|
32 val t = str2term "(2 log x) = 3"; |
|
33 val t = str2term "matches ((?a log x) = ?b) ((2 log x) = 3)"; |
|
34 atomty t; |
|
35 |
|
36 |
|
37 val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"]; |
|
38 val (dI',pI',mI') = |
|
39 ("Isac.thy",["logarithmic","univariate","equation","test"], |
|
40 ["Test","solve_log"]); |
|
41 val p = e_pos'; val c = []; |
|
42 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))]; |
|
43 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
44 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; |
|
47 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
48 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
49 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
50 case nxt of ("Apply_Method",_) => () |
|
51 | _ => raise error "logexp.sml setup innsbruck"; |
|
52 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
53 |
|
54 |
|
55 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
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; |
|
58 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
|
59 show_pt pt; |
|
60 |
|
61 *-------------------------------------------------------------------*) |