1.1 --- a/src/Tools/isac/BaseDefinitions/calcelems.sml	Tue Apr 21 16:16:11 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/calcelems.sml	Tue Apr 21 16:53:17 2020 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    type pbt_ = string * (term * term)
     1.5    val update_hrls: Thy_Html.thydata -> Error_Fill_Def.errpatID list -> Thy_Html.thydata
     1.6  
     1.7 +  val knowthys: unit -> theory list
     1.8    val isabthys: unit -> theory list
     1.9    val partID': ThyC.id -> string
    1.10  

     2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue Apr 21 16:16:11 2020 +0200
     2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy	Tue Apr 21 16:53:17 2020 +0200
     2.3 @@ -652,7 +652,7 @@
     2.4        of simplification occurs right here, in the next step.\<close>
     2.5  
     2.6  ML \<open>
     2.7 -  trace_rewrite := false;
     2.8 +  Trace.trace_rewrite := false;
     2.9    val SOME fract1 =
    2.10      parseNEW ctxt "(z - 1/2)*(z - -1/4) * (A/(z - 1/2) + B/(z - -1/4))";
    2.11    (*
    2.12 @@ -1242,7 +1242,7 @@
    2.13        tree and check if every node implements that what we have wanted.\<close>
    2.14        
    2.15  ML \<open>
    2.16 -  trace_rewrite := false; (*true*)
    2.17 +  Trace.trace_rewrite := false; (*true*)
    2.18    trace_LI := false; (*true*)
    2.19    print_depth 9;
    2.20    

     3.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Tue Apr 21 16:16:11 2020 +0200
     3.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Tue Apr 21 16:53:17 2020 +0200
     3.3 @@ -55,7 +55,7 @@
     3.4  \<close>
     3.5  ML \<open>
     3.6  val SOME (t, _) = Rewrite.rewrite_set_ thy true make_polynomial t; UnparseC.term t;
     3.7 -Celem.trace_rewrite := false;
     3.8 +Celem.Trace.trace_rewrite := false;
     3.9  \<close>
    3.10  
    3.11  section \<open>Note on bound variables\<close>
    3.12 @@ -155,13 +155,13 @@
    3.13  val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
    3.14  \<close>
    3.15  text \<open>The simplifiers are quite busy when finding the above results. you can
    3.16 -  watch them at work by setting the switch 'trace_rewrite:\<close>
    3.17 +  watch them at work by setting the switch 'Trace.trace_rewrite:\<close>
    3.18  ML \<open>
    3.19 -Celem.trace_rewrite := false;
    3.20 +Celem.Trace.trace_rewrite := false;
    3.21  tracing "+++begin++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
    3.22  val SOME (t, _) = Rewrite.rewrite_set_ thy true norm_Rational t2; UnparseC.term t;
    3.23  tracing "+++end++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++";
    3.24 -Celem.trace_rewrite := false;
    3.25 +Celem.Trace.trace_rewrite := false;
    3.26  \<close>
    3.27  text \<open>You see what happend when you click the checkbox <Tracing> on the bar
    3.28    separating this window from the Output-window.

     4.1 --- a/test/Tools/isac/Knowledge/biegelinie-1.sml	Tue Apr 21 16:16:11 2020 +0200
     4.2 +++ b/test/Tools/isac/Knowledge/biegelinie-1.sml	Tue Apr 21 16:53:17 2020 +0200
     4.3 @@ -81,8 +81,8 @@
     4.4  if UnparseC.term x1__ = "0" then ()
     4.5  else error "biegelinie.sml simplify argument_in (lhs (M_b 0 = 0)";
     4.6  
     4.7 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
     4.8 -trace_rewrite:=false;
     4.9 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
    4.10 +Trace.trace_rewrite:=false;
    4.11  
    4.12  "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";
    4.13  "----------- SubProblem (_,[setzeRandbedingungen,Biegelinien] ----";

     5.1 --- a/test/Tools/isac/Knowledge/diff.sml	Tue Apr 21 16:16:11 2020 +0200
     5.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Tue Apr 21 16:53:17 2020 +0200
     5.3 @@ -326,7 +326,7 @@
     5.4  Iterator 1;
     5.5  moveActiveRoot 1;
     5.6  autoCalculate 1 CompleteCalc;
     5.7 -(* trace_rewrite := true;
     5.8 +(* Trace.trace_rewrite := true;
     5.9     trace_LI := false;
    5.10     *)
    5.11  val ((pt,p),_) = get_calc 1; show_pt pt;
    5.12 @@ -346,11 +346,11 @@
    5.13    ["diff","after_simplification"]))];
    5.14  Iterator 1;
    5.15  moveActiveRoot 1;
    5.16 -(* trace_rewrite := true;
    5.17 +(* Trace.trace_rewrite := true;
    5.18     trace_LI := true;
    5.19     *)
    5.20  autoCalculate 1 CompleteCalc;
    5.21 -(* trace_rewrite := false;
    5.22 +(* Trace.trace_rewrite := false;
    5.23     trace_LI := false;
    5.24     *)
    5.25  val ((pt,p),_) = get_calc 1; show_pt pt;

     6.1 --- a/test/Tools/isac/Knowledge/diffapp.sml	Tue Apr 21 16:16:11 2020 +0200
     6.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml	Tue Apr 21 16:53:17 2020 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4     use"diffapp.sml";
     6.5  *)
     6.6  
     6.7 -trace_rewrite := false;
     6.8 +Trace.trace_rewrite := false;
     6.9  "Contents----------------------------------------------";
    6.10  "              Specify_Problem (match_itms_oris)       ";
    6.11  "              test specify, fmz <> []                  ";
    6.12 @@ -671,9 +671,9 @@
    6.13  UnparseC.term s;
    6.14  val t = str2term 
    6.15  "(hd o filterVar A) [A = a * b, a / 2 = r * sin alpha, b / 2 = r * cos alpha]";
    6.16 -trace_rewrite := false;
    6.17 +Trace.trace_rewrite := false;
    6.18  val SOME (t',_) = rewrite_set_ thy false prog_expr t;
    6.19 -trace_rewrite:=false;
    6.20 +Trace.trace_rewrite:=false;
    6.21  val s' = UnparseC.term t';
    6.22  (*=== inhibit exn 110726=============================================================
    6.23  if s' = "A = a * b" then() else error "new behaviour with prog_expr 3.1.";

     7.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Tue Apr 21 16:16:11 2020 +0200
     7.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Tue Apr 21 16:53:17 2020 +0200
     7.3 @@ -3,7 +3,7 @@
     7.4     (c) due to copyright terms
     7.5  *)
     7.6  
     7.7 -trace_rewrite := false;
     7.8 +Trace.trace_rewrite := false;
     7.9  "-----------------------------------------------------------------";
    7.10  "table of contents -----------------------------------------------";
    7.11  "-----------------------------------------------------------------";
    7.12 @@ -360,7 +360,7 @@
    7.13            [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]"]*)
    7.14  val t = str2term ("[c, c_2] from [c, c_2] occur_exactly_in NTH 2" ^   
    7.15  		  "[c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]");
    7.16 -trace_rewrite := false;
    7.17 +Trace.trace_rewrite := false;
    7.18  val SOME (t',_) = rewrite_set_ thy false prls_triangular t;
    7.19  (*found:...
    7.20  ##  try thm: NTH_CONS
    7.21 @@ -372,7 +372,7 @@
    7.22  ###  asms accepted: ["1 < 2 + - 1"]   stored: ["1 < 2 + -1"]
    7.23  
    7.24  ... i.e Eval ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
    7.25 -trace_rewrite:=false;
    7.26 +Trace.trace_rewrite:=false;
    7.27  
    7.28  "===== case 3: relaxed preconditions for triangular system =====";
    7.29  val fmz = ["equalities [L * q_0 = c,                               \
    7.30 @@ -421,9 +421,9 @@
    7.31  val fmz = ["equalities [0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2,\
    7.32  	               \0 = -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2]", 
    7.33  	   "solveForVars [c, c_2]", "solution LL"];
    7.34 -trace_rewrite := false;
    7.35 +Trace.trace_rewrite := false;
    7.36  val matches = refine fmz ["2x2", "LINEAR","system"];
    7.37 -trace_rewrite:=false;
    7.38 +Trace.trace_rewrite:=false;
    7.39  (*default_print_depth 11;*) matches; (*default_print_depth 3;*)
    7.40  (*brought: 'False "length_ es_ = 2"'*)
    7.41  

     8.1 --- a/test/Tools/isac/Knowledge/poly.sml	Tue Apr 21 16:16:11 2020 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Tue Apr 21 16:53:17 2020 +0200
     8.3 @@ -341,7 +341,7 @@
     8.4  if UnparseC.term t' = "x * x ^^^ 2" then ()
     8.5  else error "poly.sml Poly.is'_multUnordered doesn't work";
     8.6  
     8.7 -(* 100928 trace_rewrite shows the first occurring difference in 267b:
     8.8 +(* 100928 Trace.trace_rewrite shows the first occurring difference in 267b:
     8.9  ###  rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +
    8.10   (-48 * x ^^^ 4 + 8))
    8.11  ######  rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
    8.12 @@ -575,12 +575,12 @@
    8.13  (*default_print_depth 3;*)
    8.14  (*if there is ...
    8.15  > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
    8.16 -... then trace_rewrite:*)
    8.17 +... then Trace.trace_rewrite:*)
    8.18  
    8.19  "-----2 ---";
    8.20 -trace_rewrite := false;
    8.21 +Trace.trace_rewrite := false;
    8.22  match_pbl fmz pbt;
    8.23 -trace_rewrite := false;
    8.24 +Trace.trace_rewrite := false;
    8.25  (*... if there is no rewrite, then there is something wrong with prls*)
    8.26                                
    8.27  "-----3 ---";

     9.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Apr 21 16:16:11 2020 +0200
     9.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Tue Apr 21 16:53:17 2020 +0200
     9.3 @@ -49,8 +49,8 @@
     9.4  "----------- tests on predicates in problems ---------------------";
     9.5  "----------- tests on predicates in problems ---------------------";
     9.6  "----------- tests on predicates in problems ---------------------";
     9.7 -(* trace_rewrite:=true;
     9.8 - trace_rewrite:=false;
     9.9 +(* Trace.trace_rewrite:=true;
    9.10 + Trace.trace_rewrite:=false;
    9.11  *)
    9.12   val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
    9.13   val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
    9.14 @@ -160,7 +160,7 @@
    9.15    "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
    9.16  
    9.17    (*das rewriting l"asst sich beobachten mit
    9.18 -trace_rewrite := false;
    9.19 +Trace.trace_rewrite := false;
    9.20    *)
    9.21  
    9.22  "------15.11.02 --------------------------";
    9.23 @@ -168,7 +168,7 @@
    9.24    val bdv = (Thm.term_of o the o (parse thy)) "bdv";
    9.25    val a = (Thm.term_of o the o (parse thy)) "a";
    9.26   
    9.27 -trace_rewrite := false;
    9.28 +Trace.trace_rewrite := false;
    9.29   (* Anwenden einer Regelmenge aus Termorder.ML: *)
    9.30   val SOME (t,_) =
    9.31       rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;

    10.1 --- a/test/Tools/isac/Knowledge/polyeq-2.sml	Tue Apr 21 16:16:11 2020 +0200
    10.2 +++ b/test/Tools/isac/Knowledge/polyeq-2.sml	Tue Apr 21 16:53:17 2020 +0200
    10.3 @@ -256,9 +256,9 @@
    10.4  (* the invisible parentheses are as expected *)
    10.5  
    10.6  val t = str2term "(x + 1) * (x + 2) - (3 * x - 2) ^^^ 2 - ((2 * x - 1) ^^^ 2 + (3 * x - 1) * (x + 1)) = 0";
    10.7 -trace_rewrite:=(*true*)false;
    10.8 +Trace.trace_rewrite:=(*true*)false;
    10.9  rewrite_set_ thy false expand_binoms t;
   10.10 -trace_rewrite:=false;
   10.11 +Trace.trace_rewrite:=false;
   10.12  
   10.13  
   10.14  "----------- interSteps ([1],Res); on Schalk Is86Bsp5-------------";

    11.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Tue Apr 21 16:16:11 2020 +0200
    11.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Apr 21 16:53:17 2020 +0200
    11.3 @@ -66,13 +66,13 @@
    11.4  "----------- watch order_add_mult  -------------------------------";
    11.5  "----------- watch order_add_mult  -------------------------------";
    11.6  "----- with these simple variables it works...";
    11.7 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
    11.8 -trace_rewrite:=false;
    11.9 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.10 +Trace.trace_rewrite:=false;
   11.11  val t = str2term "((a + d) + c) + b";
   11.12  val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
   11.13  if UnparseC.term t = "a + (b + (c + d))" then ()
   11.14  else error "polyminus.sml 1 watch order_add_mult";
   11.15 -trace_rewrite:=false;
   11.16 +Trace.trace_rewrite:=false;
   11.17  
   11.18  "----- the same stepwise...";
   11.19  val od = ord_make_polynomial true (@{theory "Poly"});
   11.20 @@ -169,7 +169,7 @@
   11.21  val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
   11.22  
   11.23  "======= test rewrite_, rewrite_set_";
   11.24 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.25 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.26  val erls = erls_ordne_alphabetisch;
   11.27  val t = str2term "b + a";
   11.28  val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
   11.29 @@ -227,8 +227,8 @@
   11.30  if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
   11.31  else error "polyminus.sml: verschoenere 3 + -2 * e ...";
   11.32  
   11.33 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.34 -trace_rewrite:=false;
   11.35 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.36 +Trace.trace_rewrite:=false;
   11.37  
   11.38  "----------- met simplification for_polynomials with_minus -------";
   11.39  "----------- met simplification for_polynomials with_minus -------";
   11.40 @@ -420,7 +420,7 @@
   11.41  applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
   11.42  val ((pt,p),_) = get_calc 1; show_pt pt;
   11.43  "----- 2 ^^^";
   11.44 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.45 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.46  val erls = erls_ordne_alphabetisch;
   11.47  val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
   11.48  val SOME (t',_) = 
   11.49 @@ -435,7 +435,7 @@
   11.50  val SOME (t',_) = 
   11.51      rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
   11.52  UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
   11.53 -trace_rewrite := false;
   11.54 +Trace.trace_rewrite := false;
   11.55  
   11.56  
   11.57  applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
   11.58 @@ -577,9 +577,9 @@
   11.59  	      (*"(~ True) = False"*)
   11.60  	      Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
   11.61  	      (*"(~ False) = True"*)];
   11.62 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.63 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.64  val SOME (t', _) = rewrite_set_ thy false prls t;
   11.65 -trace_rewrite := false;
   11.66 +Trace.trace_rewrite := false;
   11.67  
   11.68  "--- does the respective prls rewrite the whole predicate ?";
   11.69  val t = str2term 
   11.70 @@ -587,9 +587,9 @@
   11.71  	    \     matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
   11.72  	    \     matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
   11.73  	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
   11.74 -(*trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.75 +(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
   11.76  val SOME (t', _) = rewrite_set_ thy false prls t;
   11.77 -trace_rewrite := false;
   11.78 +Trace.trace_rewrite := false;
   11.79  if UnparseC.term t' = "False" then ()
   11.80  else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
   11.81  

    12.1 --- a/test/Tools/isac/Knowledge/rational.sml	Tue Apr 21 16:16:11 2020 +0200
    12.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Tue Apr 21 16:53:17 2020 +0200
    12.3 @@ -336,7 +336,7 @@
    12.4  "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    12.5  "-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    12.6  val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
    12.7 -trace_rewrite := false (*true false*);
    12.8 +Trace.trace_rewrite := false (*true false*);
    12.9  (* trace stops with ...: (and then jEdit hangs)..
   12.10  rewrite_set_ thy false norm_Rational t;
   12.11  :
   12.12 @@ -438,10 +438,10 @@
   12.13                                  (* required for applying thms in rewriting ^^^^*)
   12.14  (* we get details from here..*)
   12.15  
   12.16 -trace_rewrite := false;
   12.17 +Trace.trace_rewrite := false;
   12.18  val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
   12.19 -Celem.trace_rewrite := false;
   12.20 -(* trace_rewrite:
   12.21 +Celem.Trace.trace_rewrite := false;
   12.22 +(* Trace.trace_rewrite:
   12.23  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
   12.24                       (* |||||||||||||||||||||||||||||||||||| *)
   12.25  
   12.26 @@ -450,7 +450,7 @@
   12.27  "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
   12.28  val NONE = (*case*) check_frac_sum t (*of*)
   12.29  
   12.30 -(* trace_rewrite:
   12.31 +(* Trace.trace_rewrite:
   12.32  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
   12.33                       (*         |||||||||||||||||||||||||||| *)
   12.34  val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| GUESS 2 GUESS 2 GUESS 2 GUESS 2 *)
   12.35 @@ -481,10 +481,10 @@
   12.36                                      (*AA :: real*)
   12.37  (* we get details from here..*)
   12.38  
   12.39 -Celem.trace_rewrite := false;
   12.40 +Celem.Trace.trace_rewrite := false;
   12.41  val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
   12.42 -Celem.trace_rewrite := false;
   12.43 -(* trace_rewrite:
   12.44 +Celem.Trace.trace_rewrite := false;
   12.45 +(* Trace.trace_rewrite:
   12.46  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
   12.47                       (* |||||||||||||||||||||||||||||||||||| *)
   12.48  val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| *)
   12.49 @@ -492,7 +492,7 @@
   12.50  "~~~~~ fun add_fraction_p_ , ad-hoc args:"; val (t) = (t);
   12.51  val NONE = (*case*) check_frac_sum t (*of*)
   12.52  
   12.53 -(* trace_rewrite:
   12.54 +(* Trace.trace_rewrite:
   12.55  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + -1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
   12.56                       (*         |||||||||||||||||||||||||||| *)
   12.57  val t = (the o (parseNEW  ctxt))(* ||||||||||||||||||||||||| *)
   12.58 @@ -752,7 +752,7 @@
   12.59  (* simpler variant *)
   12.60  val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty [Rls_ cancel_p, Rls_ add_fractions_p]
   12.61  val SOME (t', asm) = rewrite_set_ thy false testrls t;
   12.62 -(*trace_rewrite := false;
   12.63 +(*Trace.trace_rewrite := false;
   12.64  #  rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
   12.65  ##  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
   12.66  ##  rls: add_fractions_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f 
   12.67 @@ -949,7 +949,7 @@
   12.68  if UnparseC.term t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
   12.69  else error "rational.sml 3";
   12.70  
   12.71 -(*trace_rewrite:=true;*)
   12.72 +(*Trace.trace_rewrite:=true;*)
   12.73  val t = str2term "Not (6*x is_atom)";
   12.74  val SOME (t',_) = rewrite_set_ thy false powers_erls t; UnparseC.term t';
   12.75  "HOL.True";
   12.76 @@ -1807,7 +1807,7 @@
   12.77  val t = str2term 
   12.78    ("((a^^^2 - b^^^2)/(2*a*b) + 2*a*b/(a^^^2 - b^^^2))  /  ((a^^^2 + b^^^2)/(2*a*b) + 1)    / " ^
   12.79     "((a^^^2 + b^^^2)^^^2  /  (a + b)^^^2)");
   12.80 -(* trace_rewrite := true;
   12.81 +(* Trace.trace_rewrite := true;
   12.82  rewrite_set_ thy false norm_Rational t;
   12.83  :
   12.84  ####  rls: cancel_p on: (2 * (a ^^^ 7 * b) + 4 * (a ^^^ 6 * b ^^^ 2) + 6 * (a ^^^ 5 * b ^^^ 3) +
   12.85 @@ -1830,7 +1830,7 @@
   12.86  "-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?";
   12.87  val t = str2term ("(1/x + 1/y + 1/z)  /  (1/x - 1/y - 1/z)  /  " ^
   12.88    "(2*x^^^2 / (x^^^2 - z^^^2) / (x / (x + z)  +  x / (x - z)))");
   12.89 -(* trace_rewrite := true;
   12.90 +(* Trace.trace_rewrite := true;
   12.91  rewrite_set_ thy false norm_Rational t;
   12.92  :
   12.93  ####  rls: cancel_p on: (2 * (x ^^^ 6 * (y ^^^ 2 * z)) + 2 * (x ^^^ 6 * (y * z ^^^ 2)) +
   12.94 @@ -1860,7 +1860,7 @@
   12.95  
   12.96  anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
   12.97  
   12.98 -"-------- Schalk I, p.70 Nr. 480b: terms are exploding, trace_rewrite stops at";
   12.99 +"-------- Schalk I, p.70 Nr. 480b: terms are exploding, Trace.trace_rewrite stops at";
  12.100  val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
  12.101  		 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
  12.102  		 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^

    13.1 --- a/test/Tools/isac/Knowledge/rlang.sml	Tue Apr 21 16:16:11 2020 +0200
    13.2 +++ b/test/Tools/isac/Knowledge/rlang.sml	Tue Apr 21 16:53:17 2020 +0200
    13.3 @@ -50,8 +50,8 @@
    13.4  }
    13.5  *)
    13.6  
    13.7 -(* trace_rewrite:=true;
    13.8 - trace_rewrite:=false;
    13.9 +(* Trace.trace_rewrite:=true;
   13.10 + Trace.trace_rewrite:=false;
   13.11   refine fmz ["univariate","equation"];
   13.12  *)
   13.13  "---- rlang.sml begin-----------------------------------";
   13.14 @@ -353,7 +353,7 @@
   13.15  val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
   13.16  val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
   13.17  val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
   13.18 -(*trace_rewrite:=true;
   13.19 +(*Trace.trace_rewrite:=true;
   13.20  *)
   13.21  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   13.22  val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   13.23 @@ -1419,10 +1419,10 @@
   13.24  
   13.25  
   13.26  val t = str2term"(a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) =\n4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)";
   13.27 -trace_rewrite := false;
   13.28 +Trace.trace_rewrite := false;
   13.29  val SOME (t',asm) = rewrite_set_ thy false norm_Rational t;
   13.30  UnparseC.term t';
   13.31 -trace_rewrite:=false;
   13.32 +Trace.trace_rewrite:=false;
   13.33  
   13.34  #  rls: norm_Rational on: (a + b * x) / (a + -1 * (b * x)) + -1 * (a + -1 * (b * x)) / (a + b * x) = 4 * a * b / (a ^^^ 2 + -1 * b ^^^ 2)
   13.35  
   13.36 @@ -1635,7 +1635,7 @@
   13.37  "------ rlang.sml end---------------------------------";
   13.38  
   13.39  (*------------------------------vvv-Rewrite_Set "rat_eliminate"---------
   13.40 -> trace_rewrite:=true;
   13.41 +> Trace.trace_rewrite:=true;
   13.42  > val t = str2term 
   13.43    "(3 + -1 * x + 1 * x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3) = 1 / x";
   13.44  > val SOME (t',asm) = 
   13.45 @@ -1643,7 +1643,7 @@
   13.46  > UnparseC.term t'; UnparseC.terms asm;
   13.47  "(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3)"
   13.48  "[\"9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0\",\"x ~= 0\"]"
   13.49 -> trace_rewrite:=false;
   13.50 +> Trace.trace_rewrite:=false;
   13.51    ------------------------------^^^-Rewrite_Set "rat_eliminate"---------*)
   13.52  
   13.53  

    14.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 21 16:16:11 2020 +0200
    14.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Apr 21 16:53:17 2020 +0200
    14.3 @@ -246,8 +246,8 @@
    14.4  (writeln o UnparseC.term) t;
    14.5  if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
    14.6  then () else error "rewrite.sml rewrite_inst_ bdvs";
    14.7 -> trace_rewrite:=true;
    14.8 -trace_rewrite:=false;--------------------------------------------*)
    14.9 +> Trace.trace_rewrite:=true;
   14.10 +Trace.trace_rewrite:=false;--------------------------------------------*)
   14.11  
   14.12  
   14.13  "----------- check diff 2002--2009-3 --------------------";
   14.14 @@ -327,7 +327,7 @@
   14.15  writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
   14.16  val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
   14.17  UnparseC.term t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
   14.18 -(*checked visually: trace_rewrite looks like above for 2009*)
   14.19 +(*checked visually: Trace.trace_rewrite looks like above for 2009*)
   14.20  
   14.21  writeln "----- rewrite_ rat_mult_poly_r--------------------------";
   14.22  val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
   14.23 @@ -422,9 +422,9 @@
   14.24                            Const ("HOL.True", _))) => ()
   14.25    | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
   14.26  
   14.27 -tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
   14.28 +tracing "----- begin rewrite x^^^2 * x ---"; Trace.trace_rewrite := false;
   14.29  val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
   14.30 -tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
   14.31 +tracing "----- end rewrite x^^^2 * x ---"; Trace.trace_rewrite := false;
   14.32  if UnparseC.term t' = "x * x ^^^ 2" then ()
   14.33  else error "rewrite.sml Poly.is'_multUnordered doesn't work";
   14.34  
   14.35 @@ -655,7 +655,7 @@
   14.36  
   14.37             rewrite__set_ thy (i + 1) false bdv rls a (*of*);
   14.38  
   14.39 -(*+*)trace_rewrite := true;
   14.40 +(*+*)Trace.trace_rewrite := true;
   14.41  
   14.42          (*this was False; vvvv--- means: indeterminate*)
   14.43      val (* SOME (t, a') *)NONE = (*case*)
   14.44 @@ -676,7 +676,7 @@
   14.45   :                             
   14.46   ###  asms accepted: [x \<noteq> 0]   stored: []
   14.47   : *)
   14.48 -trace_rewrite := false;
   14.49 +Trace.trace_rewrite := false;
   14.50  ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
   14.51  
   14.52  

    15.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Apr 21 16:16:11 2020 +0200
    15.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Apr 21 16:53:17 2020 +0200
    15.3 @@ -1,5 +1,5 @@
    15.4 -(* trace_rewrite:= true;
    15.5 -   trace_rewrite:= false;
    15.6 +(* Trace.trace_rewrite:= true;
    15.7 +   Trace.trace_rewrite:= false;
    15.8  
    15.9     method "sqrt-equ-test", _NOT_ "square-equation" 
   15.10  *)
   15.11 @@ -546,8 +546,8 @@
   15.12   val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
   15.13   val SOME (t',asm) = rewrite_set_ thy false rls t;
   15.14   UnparseC.term t';
   15.15 -> trace_rewrite:=true; 
   15.16 - trace_rewrite:=false; 
   15.17 +> Trace.trace_rewrite:=true; 
   15.18 + Trace.trace_rewrite:=false; 
   15.19  *)
   15.20  
   15.21  (*me------------

    16.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml	Tue Apr 21 16:16:11 2020 +0200
    16.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml	Tue Apr 21 16:53:17 2020 +0200
    16.3 @@ -402,9 +402,9 @@
    16.4        "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b ^^^ 2)"))*)
    16.5  Ctree.get_assumptions pt p;
    16.6  (*it = [] : string list;*)
    16.7 -trace_rewrite := false;
    16.8 +Trace.trace_rewrite := false;
    16.9  val (p,_,f,nxt,_,pt) = me nxt p c pt;
   16.10 -trace_rewrite := false;
   16.11 +Trace.trace_rewrite := false;
   16.12  val asms = Ctree.get_assumptions pt p;
   16.13  if asms = [(str2term "0 <= 9 + 4 * x",[1]),
   16.14  	   (str2term "0 <= x",[1]),

    17.1 --- a/test/Tools/isac/ProgLang/calculate.sml	Tue Apr 21 16:16:11 2020 +0200
    17.2 +++ b/test/Tools/isac/ProgLang/calculate.sml	Tue Apr 21 16:53:17 2020 +0200
    17.3 @@ -148,7 +148,7 @@
    17.4  "----------- check calculate bottom up ------------------";
    17.5  "----------- check calculate bottom up ------------------";
    17.6  (*-------------- eval_cancel works: *)
    17.7 - trace_rewrite:=false;
    17.8 + Trace.trace_rewrite:=false;
    17.9   val thy = @{theory Test};
   17.10   val rls = Test_simplify;
   17.11   val t = (Thm.term_of o the o (parse thy)) "(-4) / 2";
   17.12 @@ -166,9 +166,9 @@
   17.13    SOME (Const ("Groups.plus_class.plus", _) $ Free ("2", _) $ Free ("x", _), []) => ()
   17.14  | _ => error "rewrite_set_ (3+1+2*x)/2 changed";
   17.15  
   17.16 - trace_rewrite:=false; (*=true3.6.03*)
   17.17 + Trace.trace_rewrite:=false; (*=true3.6.03*)
   17.18  
   17.19 -(*--- trace_rewrite before correction of ... --------------------
   17.20 +(*--- Trace.trace_rewrite before correction of ... --------------------
   17.21   val ct = "(-3 + 2 * x + -1) / 2";
   17.22   val (ct,_) = the (rewrite_set thy'  false rls ct);
   17.23  :
   17.24 @@ -197,7 +197,7 @@
   17.25  
   17.26  
   17.27  (*===================*)
   17.28 - trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
   17.29 + Trace.trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
   17.30   val t = (Thm.term_of o the o (parse thy))  "x + (-1 + -3) / 2";
   17.31  val SOME (res, []) = rewrite_set_ thy false rls t;
   17.32  if UnparseC.term res = "-2 + x" then () else error "rewrite_set_  x + (-1 + -3) / 2  changed";
   17.33 @@ -215,7 +215,7 @@
   17.34  ### trying calc. 'pow'
   17.35  *)
   17.36  
   17.37 - trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
   17.38 + Trace.trace_rewrite:=false; (*WN130722: =true stopped Test_Isac.thy*)
   17.39  
   17.40  "----------- Prog_Expr.pow Power.power_class.power ---------";
   17.41  "----------- Prog_Expr.pow Power.power_class.power ---------";

    18.1 --- a/test/Tools/isac/ProgLang/listC.sml	Tue Apr 21 16:16:11 2020 +0200
    18.2 +++ b/test/Tools/isac/ProgLang/listC.sml	Tue Apr 21 16:53:17 2020 +0200
    18.3 @@ -63,9 +63,9 @@
    18.4  (* now the argument "(3 + - 1)" etc needs to be evaluated in the assumption of NTH_CONS *)
    18.5  val t = str2term "NTH 3 [a,b,c,d,e]";
    18.6  atomty t;
    18.7 -trace_rewrite := false;
    18.8 +Trace.trace_rewrite := false;
    18.9  val SOME (t', _) = rewrite_set_ thy false prog_expr t;
   18.10 -trace_rewrite := false;
   18.11 +Trace.trace_rewrite := false;
   18.12  if UnparseC.term t' = "c" then () 
   18.13  else error "NTH 3 [a,b,c,d,e] = c ..changed";
   18.14  

    19.1 --- a/test/Tools/isac/ProgLang/prog_expr.sml	Tue Apr 21 16:16:11 2020 +0200
    19.2 +++ b/test/Tools/isac/ProgLang/prog_expr.sml	Tue Apr 21 16:53:17 2020 +0200
    19.3 @@ -230,14 +230,14 @@
    19.4  if UnparseC.term pred = "boollist2sum\n [b1 = k - 2 * q, b2 = k - 2 * q, b3 = k - 2 * q, b4 = k - 2 * q] =\nb1 + b2 + b3 + b4" then () 
    19.5  else error "atools.sml diff.behav. in eval_boollist2sum";
    19.6  
    19.7 -trace_rewrite := false;
    19.8 +Trace.trace_rewrite := false;
    19.9  val srls_ = Rule_Set.append_rules "srls_..Berechnung-erstSymbolisch" Rule_Set.empty 
   19.10  		      [Eval ("Prog_Expr.boollist2sum", eval_boollist2sum "")];
   19.11  val t = str2t 
   19.12         "boollist2sum [b1 = k - 2*q, b2 = k - 2*q, b3 = k - 2*q, b4 = k - 2*q]";
   19.13  case rewrite_set_ thy false srls_ t of SOME _ => ()
   19.14  | _ => error "atools.sml diff.rewrite boollist2sum";
   19.15 -trace_rewrite := false;
   19.16 +Trace.trace_rewrite := false;
   19.17  
   19.18  
   19.19  "---------fun eval_binop -----------------------------------------------------------------------";