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 ?
walther@59997: Refine.refine ["equality ((2 log x) = 3)", "solveFor x", "solutions L"] 
walther@59997:        ["equation", "test"]; *)
neuper@37906: *)
neuper@37906: 
Walther@60565: val t = TermC.parse_test @{context} "(2 log x)";
Walther@60565: val t = TermC.parse_test @{context} "(2 log x) = 3";
Walther@60565: val t = TermC.parse_test @{context} "matches ((?a log x) = ?b) ((2 log x) = 3)";
Walther@60650: TermC.atom_trace_detail @{context} t;
neuper@37906: 
neuper@37906: 
walther@59997: val fmz = ["equality ((2 log x) = 3)", "solveFor x", "solutions L"];
neuper@37906: val (dI',pI',mI') =
walther@59997:   ("Isac_Knowledge",["logarithmic", "univariate", "equation", "test"],
walther@59997:    ["Test", "solve_log"]);
neuper@37906: val p = e_pos'; val c = []; 
t@42206: (*============ inhibit exn 110726 ==============================================
Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(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;
walther@59983: Test_Tool.show_pt pt;
t@42206: ============ inhibit exn 110726 ==============================================*)
neuper@37906: