1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Sun Jul 21 15:15:50 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Mon Jul 22 13:52:18 2013 +0200
     1.3 @@ -2,9 +2,6 @@
     1.4     author: Walther Neuper
     1.5     WN071207,
     1.6     (c) due to copyright terms
     1.7 -
     1.8 -use"../smltest/IsacKnowledge/polyminus.sml";
     1.9 -use"polyminus.sml";
    1.10  *)
    1.11  "--------------------------------------------------------";
    1.12  "--------------------------------------------------------";
    1.13 @@ -69,7 +66,7 @@
    1.14  "----------- watch order_add_mult  -------------------------------";
    1.15  "----------- watch order_add_mult  -------------------------------";
    1.16  "----- with these simple variables it works...";
    1.17 -trace_rewrite:=true;
    1.18 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.19  trace_rewrite:=false;
    1.20  val t = str2term "((a + d) + c) + b";
    1.21  val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;
    1.22 @@ -172,7 +169,7 @@
    1.23  val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t;
    1.24  
    1.25  "======= test rewrite_, rewrite_set_";
    1.26 -trace_rewrite:=true;
    1.27 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.28  val erls = erls_ordne_alphabetisch;
    1.29  val t = str2term "b + a";
    1.30  val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;
    1.31 @@ -230,7 +227,7 @@
    1.32  if term2str t = "3 - 2 * e + 2 * f + 2 * g" then ()
    1.33  else error "polyminus.sml: verschoenere 3 + -2 * e ...";
    1.34  
    1.35 -trace_rewrite:=true;
    1.36 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.37  trace_rewrite:=false;
    1.38  
    1.39  "----------- met simplification for_polynomials with_minus -------";
    1.40 @@ -422,7 +419,7 @@
    1.41  applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
    1.42  val ((pt,p),_) = get_calc 1; show_pt pt;
    1.43  "----- 2 ^^^";
    1.44 -trace_rewrite := true;
    1.45 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.46  val erls = erls_ordne_alphabetisch;
    1.47  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
    1.48  val SOME (t',_) = 
    1.49 @@ -579,7 +576,7 @@
    1.50  	      (*"(~ True) = False"*)
    1.51  	      Thm ("not_false",num_str @{thm not_false})
    1.52  	      (*"(~ False) = True"*)];
    1.53 -trace_rewrite := true;
    1.54 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.55  val SOME (t', _) = rewrite_set_ thy false prls t;
    1.56  trace_rewrite := false;
    1.57  
    1.58 @@ -589,7 +586,7 @@
    1.59  	    \     matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
    1.60  	    \     matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
    1.61  	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
    1.62 -trace_rewrite := true;
    1.63 +(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.64  val SOME (t', _) = rewrite_set_ thy false prls t;
    1.65  trace_rewrite := false;
    1.66  if term2str t' = "False" then ()