test/Tools/isac/Knowledge/logexp.sml
branchdecompose-isar
changeset 42206 83165a8623dc
parent 41943 f33f6959948b
child 42321 e68b4b4f0fac
     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 ?===========================================================*)