tuned decompose-isar
authorThomas Leh <t.leh@gmx.at>
Tue, 26 Jul 2011 16:50:27 +0200
branchdecompose-isar
changeset 4220683165a8623dc
parent 42205 2910634f8537
child 42208 35c81506697d
child 42211 51c3c007d7fd
tuned
test/Tools/isac/Knowledge/logexp.sml
test/Tools/isac/Test_Isac.thy
test/Tools/isac/Test_Some.thy
     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 ?===========================================================*)
     2.1 --- a/test/Tools/isac/Test_Isac.thy	Tue Jul 26 16:15:03 2011 +0200
     2.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue Jul 26 16:50:27 2011 +0200
     2.3 @@ -161,8 +161,8 @@
     2.4  (*use "Knowledge/polyeq.sml"           2002*)
     2.5  (*use "Knowledge/rlang.sml"            2002???*)
     2.6    use "Knowledge/calculus.sml"       (*new 2011*)
     2.7 -(*use "Knowledge/trig.sml"             2002*)
     2.8 -(*use "Knowledge/logexp.sml"           2002*)
     2.9 +  use "Knowledge/trig.sml"           (*complete*)
    2.10 +  use "Knowledge/logexp.sml"         (*part.*) 
    2.11    use "Knowledge/diff.sml"           (*part.*)
    2.12    use "Knowledge/integrate.sml"      (*part. was complete 2009-2
    2.13                                                diff.emacs--jedit*)
     3.1 --- a/test/Tools/isac/Test_Some.thy	Tue Jul 26 16:15:03 2011 +0200
     3.2 +++ b/test/Tools/isac/Test_Some.thy	Tue Jul 26 16:50:27 2011 +0200
     3.3 @@ -7,21 +7,11 @@
     3.4  
     3.5  ML{* writeln "**** run the test ***************************************" *}
     3.6  
     3.7 -use"../../../test/Tools/isac/Interpret/appl.sml" 
     3.8 +use"../../../test/Tools/isac/Knowledge/logexp.sml" 
     3.9  
    3.10  ML {*
    3.11  
    3.12  
    3.13 -
    3.14 -
    3.15 -
    3.16 -
    3.17 -
    3.18 -
    3.19 -
    3.20 -
    3.21 -
    3.22 -
    3.23  *}
    3.24  ML{*
    3.25  *}
    3.26 @@ -35,8 +25,8 @@
    3.27  end
    3.28  
    3.29  
    3.30 -(*============ inhibit exn AK110725 ==============================================
    3.31 -============ inhibit exn AK110725 ==============================================*)
    3.32 +(*============ inhibit exn 110726 ==============================================
    3.33 +============ inhibit exn 110726 ==============================================*)
    3.34  
    3.35  
    3.36  (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.