1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Apr 21 16:16:11 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Apr 21 16:53:17 2020 +0200
     1.3 @@ -66,13 +66,13 @@
     1.4  "----------- watch order_add_mult  -------------------------------";
     1.5  "----------- watch order_add_mult  -------------------------------";
     1.6  "----- with these simple variables it works...";
     1.7 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
     1.8 -trace_rewrite:=false;
     1.9 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.10 +Trace.trace_rewrite:=false;
    1.11  val t = str2term "((a + d) + c) + b";
    1.12  val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
    1.13  if UnparseC.term t = "a + (b + (c + d))" then ()
    1.14  else error "polyminus.sml 1 watch order_add_mult";
    1.15 -trace_rewrite:=false;
    1.16 +Trace.trace_rewrite:=false;
    1.17  
    1.18  "----- the same stepwise...";
    1.19  val od = ord_make_polynomial true (@{theory "Poly"});
    1.20 @@ -169,7 +169,7 @@
    1.21  val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
    1.22  
    1.23  "======= test rewrite_, rewrite_set_";
    1.24 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.25 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.26  val erls = erls_ordne_alphabetisch;
    1.27  val t = str2term "b + a";
    1.28  val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
    1.29 @@ -227,8 +227,8 @@
    1.30  if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
    1.31  else error "polyminus.sml: verschoenere 3 + -2 * e ...";
    1.32  
    1.33 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.34 -trace_rewrite:=false;
    1.35 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.36 +Trace.trace_rewrite:=false;
    1.37  
    1.38  "----------- met simplification for_polynomials with_minus -------";
    1.39  "----------- met simplification for_polynomials with_minus -------";
    1.40 @@ -420,7 +420,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; ..stopped Test_Isac.thy*)
    1.45 +(*Trace.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 @@ -435,7 +435,7 @@
    1.50  val SOME (t',_) = 
    1.51      rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
    1.52  UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
    1.53 -trace_rewrite := false;
    1.54 +Trace.trace_rewrite := false;
    1.55  
    1.56  
    1.57  applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
    1.58 @@ -577,9 +577,9 @@
    1.59  	      (*"(~ True) = False"*)
    1.60  	      Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
    1.61  	      (*"(~ False) = True"*)];
    1.62 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.63 +(*Trace.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 +Trace.trace_rewrite := false;
    1.67  
    1.68  "--- does the respective prls rewrite the whole predicate ?";
    1.69  val t = str2term 
    1.70 @@ -587,9 +587,9 @@
    1.71  	    \     matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
    1.72  	    \     matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
    1.73  	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
    1.74 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.75 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
    1.76  val SOME (t', _) = rewrite_set_ thy false prls t;
    1.77 -trace_rewrite := false;
    1.78 +Trace.trace_rewrite := false;
    1.79  if UnparseC.term t' = "False" then ()
    1.80  else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
    1.81