t@42206: 
neuper@42321: (* Title:  test/../logexp.sml
neuper@42321:    Author: Walther Neuper 110320
neuper@42321:    (c) copyright due to lincense terms.
neuper@37906: *)
neuper@37906: 
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "table of contents -----------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "----------- setup presentation innsbruck ------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: "-----------------------------------------------------------------";
neuper@37906: 
t@42206: val thy = @{theory "LogExp"};
neuper@37906: 
neuper@37906: "----------- setup presentation innsbruck ------------------------";
neuper@37906: "----------- setup presentation innsbruck ------------------------";
neuper@37906: "----------- setup presentation innsbruck ------------------------";
neuper@37906: (*
neuper@37906: NOT INCLUDED IN ROOT.ML and RTEST-root.sml, since the pbl and met
neuper@37906: defined in IsacKnowledge/Test.ML are out-commented
neuper@37906: in order to allow for demonstration of authoring !
neuper@37906: 
neuper@37906: equality_power;
neuper@37906: exp_invers_log;
wneuper@59592: (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ?
neuper@37906: refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"] 
t@42206:        ["equation","test"]; *)
neuper@37906: *)
neuper@37906: 
neuper@37906: val t = str2term "(2 log x)";
neuper@37906: val t = str2term "(2 log x) = 3";
neuper@37906: val t = str2term "matches ((?a log x) = ?b) ((2 log x) = 3)";
neuper@37906: atomty t;
neuper@37906: 
neuper@37906: 
neuper@37906: val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"];
neuper@37906: val (dI',pI',mI') =
wneuper@59592:   ("Isac_Knowledge",["logarithmic","univariate","equation","test"],
neuper@37906:    ["Test","solve_log"]);
neuper@37906: val p = e_pos'; val c = []; 
t@42206: (*============ inhibit exn 110726 ==============================================
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: case nxt of ("Apply_Method",_) => ()
neuper@38031: 	  | _ => error "logexp.sml setup innsbruck";
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
neuper@37906: 
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
neuper@37906: show_pt pt;
t@42206: ============ inhibit exn 110726 ==============================================*)
neuper@37906: