|
t@42206
|
1 |
|
|
neuper@42321
|
2 |
(* Title: test/../logexp.sml
|
|
neuper@42321
|
3 |
Author: Walther Neuper 110320
|
|
neuper@42321
|
4 |
(c) copyright due to lincense terms.
|
|
neuper@37906
|
5 |
*)
|
|
neuper@37906
|
6 |
|
|
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 |
|
|
t@42206
|
15 |
val thy = @{theory "LogExp"};
|
|
neuper@37906
|
16 |
|
|
neuper@37906
|
17 |
"----------- setup presentation innsbruck ------------------------";
|
|
neuper@37906
|
18 |
"----------- setup presentation innsbruck ------------------------";
|
|
neuper@37906
|
19 |
"----------- setup presentation innsbruck ------------------------";
|
|
neuper@37906
|
20 |
(*
|
|
neuper@37906
|
21 |
NOT INCLUDED IN ROOT.ML and RTEST-root.sml, since the pbl and met
|
|
neuper@37906
|
22 |
defined in IsacKnowledge/Test.ML are out-commented
|
|
neuper@37906
|
23 |
in order to allow for demonstration of authoring !
|
|
neuper@37906
|
24 |
|
|
neuper@37906
|
25 |
equality_power;
|
|
neuper@37906
|
26 |
exp_invers_log;
|
|
wneuper@59592
|
27 |
(* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ?
|
|
walther@59997
|
28 |
Refine.refine ["equality ((2 log x) = 3)", "solveFor x", "solutions L"]
|
|
walther@59997
|
29 |
["equation", "test"]; *)
|
|
neuper@37906
|
30 |
*)
|
|
neuper@37906
|
31 |
|
|
Walther@60565
|
32 |
val t = TermC.parse_test @{context} "(2 log x)";
|
|
Walther@60565
|
33 |
val t = TermC.parse_test @{context} "(2 log x) = 3";
|
|
Walther@60565
|
34 |
val t = TermC.parse_test @{context} "matches ((?a log x) = ?b) ((2 log x) = 3)";
|
|
Walther@60650
|
35 |
TermC.atom_trace_detail @{context} t;
|
|
neuper@37906
|
36 |
|
|
neuper@37906
|
37 |
|
|
walther@59997
|
38 |
val fmz = ["equality ((2 log x) = 3)", "solveFor x", "solutions L"];
|
|
neuper@37906
|
39 |
val (dI',pI',mI') =
|
|
walther@59997
|
40 |
("Isac_Knowledge",["logarithmic", "univariate", "equation", "test"],
|
|
walther@59997
|
41 |
["Test", "solve_log"]);
|
|
neuper@37906
|
42 |
val p = e_pos'; val c = [];
|
|
t@42206
|
43 |
(*============ inhibit exn 110726 ==============================================
|
|
Walther@60571
|
44 |
val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
|
|
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 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
51 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;
|
|
neuper@37906
|
52 |
case nxt of ("Apply_Method",_) => ()
|
|
neuper@38031
|
53 |
| _ => error "logexp.sml setup innsbruck";
|
|
neuper@37906
|
54 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
|
neuper@37906
|
55 |
|
|
neuper@37906
|
56 |
|
|
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 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
|
neuper@37906
|
60 |
val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
|
|
walther@59983
|
61 |
Test_Tool.show_pt pt;
|
|
t@42206
|
62 |
============ inhibit exn 110726 ==============================================*)
|
|
neuper@37906
|
63 |
|