1 (* testexamples for LogExp, logarithms and exponential functions and terms
3 use"../smltest/IsacKnowledge/logexp.sml";
7 "-----------------------------------------------------------------";
8 "table of contents -----------------------------------------------";
9 "-----------------------------------------------------------------";
10 "----------- setup presentation innsbruck ------------------------";
11 "-----------------------------------------------------------------";
12 "-----------------------------------------------------------------";
13 "-----------------------------------------------------------------";
16 "----------- setup presentation innsbruck ------------------------";
17 "----------- setup presentation innsbruck ------------------------";
18 "----------- setup presentation innsbruck ------------------------";
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 !
26 (* WN071203 ???... wrong thy ?!? because parsing with Isac.thy works ?
27 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"]
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)";
37 val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"];
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;
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;
61 *-------------------------------------------------------------------*)