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