prep. remove Specify/mstools.sml
2 (* Title: test/../logexp.sml
3 Author: Walther Neuper 110320
4 (c) copyright due to lincense terms.
7 "-----------------------------------------------------------------";
8 "table of contents -----------------------------------------------";
9 "-----------------------------------------------------------------";
10 "----------- setup presentation innsbruck ------------------------";
11 "-----------------------------------------------------------------";
12 "-----------------------------------------------------------------";
13 "-----------------------------------------------------------------";
15 val thy = @{theory "LogExp"};
17 "----------- setup presentation innsbruck ------------------------";
18 "----------- setup presentation innsbruck ------------------------";
19 "----------- setup presentation innsbruck ------------------------";
21 NOT INCLUDED IN ROOT.ML and RTEST-root.sml, since the pbl and met
22 defined in IsacKnowledge/Test.ML are out-commented
23 in order to allow for demonstration of authoring !
27 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ?
28 Specify.refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"]
29 ["equation","test"]; *)
32 val t = str2term "(2 log x)";
33 val t = str2term "(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"];
40 ("Isac_Knowledge",["logarithmic","univariate","equation","test"],
41 ["Test","solve_log"]);
42 val p = e_pos'; val c = [];
43 (*============ inhibit exn 110726 ==============================================
44 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p c pt;
51 val (p,_,f,nxt,_,pt) = me nxt p c pt;
52 case nxt of ("Apply_Method",_) => ()
53 | _ => error "logexp.sml setup innsbruck";
54 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 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;
62 ============ inhibit exn 110726 ==============================================*)