1.1 --- a/test/Tools/isac/Knowledge/logexp.sml Tue Jul 26 16:15:03 2011 +0200
1.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Tue Jul 26 16:50:27 2011 +0200
1.3 @@ -1,3 +1,4 @@
1.4 +
1.5 (* testexamples for LogExp, logarithms and exponential functions and terms
1.6
1.7 use"../smltest/IsacKnowledge/logexp.sml";
1.8 @@ -11,8 +12,7 @@
1.9 "-----------------------------------------------------------------";
1.10 "-----------------------------------------------------------------";
1.11
1.12 -(*=== inhibit exn ?=============================================================
1.13 -val thy = LogExp.thy;
1.14 +val thy = @{theory "LogExp"};
1.15
1.16 "----------- setup presentation innsbruck ------------------------";
1.17 "----------- setup presentation innsbruck ------------------------";
1.18 @@ -26,7 +26,7 @@
1.19 exp_invers_log;
1.20 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac") works ?
1.21 refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"]
1.22 - ["equation","test"];
1.23 + ["equation","test"]; *)
1.24 *)
1.25
1.26 val t = str2term "(2 log x)";
1.27 @@ -40,6 +40,7 @@
1.28 ("Isac",["logarithmic","univariate","equation","test"],
1.29 ["Test","solve_log"]);
1.30 val p = e_pos'; val c = [];
1.31 +(*============ inhibit exn 110726 ==============================================
1.32 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.33 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.34 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.35 @@ -58,6 +59,5 @@
1.36 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.37 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
1.38 show_pt pt;
1.39 +============ inhibit exn 110726 ==============================================*)
1.40
1.41 -*-------------------------------------------------------------------*)
1.42 -===== inhibit exn ?===========================================================*)