1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml	Sat Jul 17 14:05:28 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml	Sun Jul 18 16:20:32 2021 +0200
     1.3 @@ -378,9 +378,9 @@
     1.4                                  (* required for applying thms in rewriting  \<up> ^*)
     1.5  (* we get details from here..*)
     1.6  
     1.7 -Rewrite.trace_on := false;
     1.8 +Rewrite.trace_on := false; (*true false*)
     1.9  val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
    1.10 -Rewrite.trace_on := false;
    1.11 +Rewrite.trace_on := false; (*true false*)
    1.12  (* Rewrite.trace_on:
    1.13  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
    1.14                       (* |||||||||||||||||||||||||||||||||||| *)
    1.15 @@ -421,9 +421,9 @@
    1.16                                      (*AA :: real*)
    1.17  (* we get details from here..*)
    1.18  
    1.19 -Rewrite.trace_on := false;
    1.20 +Rewrite.trace_on := false; (*true false*)
    1.21  val SOME (t', _) = Rewrite.rewrite_set_ thy true add_fractions_p t;
    1.22 -Rewrite.trace_on := false;
    1.23 +Rewrite.trace_on := false; (*true false*)
    1.24  (* Rewrite.trace_on:
    1.25  add_fractions_p on: 3 = A / 2 + A / 4 + (B / 2 + - 1 * B / 2) --> 3 = A / 2 + A / 4 + 0 / 2 *)
    1.26                       (* |||||||||||||||||||||||||||||||||||| *)
    1.27 @@ -693,7 +693,7 @@
    1.28  (* simpler variant *)
    1.29  val testrls = Rule_Set.append_rules "testrls" Rule_Set.empty [Rls_ cancel_p, Rls_ add_fractions_p]
    1.30  val SOME (t', asm) = rewrite_set_ thy false testrls t;
    1.31 -(*Rewrite.trace_on := false;
    1.32 +(*Rewrite.trace_on := false; (*true false*)
    1.33  #  rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
    1.34  ##  rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x) 
    1.35  ##  rls: add_fractions_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f 
    1.36 @@ -880,7 +880,8 @@
    1.37  "-------- examples: rls norm_Rational ----------------------------------------";
    1.38  "-------- examples: rls norm_Rational ----------------------------------------";
    1.39  "-------- examples: rls norm_Rational ----------------------------------------";
    1.40 -(*Rewrite.trace_on:=true;*)
    1.41 +Rewrite.trace_on := false; (*true false*)
    1.42 +
    1.43  val t = TermC.str2term "Not (6*x is_atom)";
    1.44  val SOME (t',_) = rewrite_set_ thy false powers_erls t; UnparseC.term t';
    1.45  "HOL.True";
    1.46 @@ -1721,7 +1722,7 @@
    1.47  val t = TermC.str2term 
    1.48    ("((a \<up> 2 - b \<up> 2)/(2*a*b) + 2*a*b/(a \<up> 2 - b \<up> 2))  /  ((a \<up> 2 + b \<up> 2)/(2*a*b) + 1)    / " ^
    1.49     "((a \<up> 2 + b \<up> 2) \<up> 2  /  (a + b) \<up> 2)");
    1.50 -(* Rewrite.trace_on := true;
    1.51 +(* Rewrite.trace_on := true; (*true false*)
    1.52  rewrite_set_ thy false norm_Rational t;
    1.53  :
    1.54  ####  rls: cancel_p on: (2 * (a \<up> 7 * b) + 4 * (a \<up> 6 * b \<up> 2) + 6 * (a \<up> 5 * b \<up> 3) +
    1.55 @@ -1744,7 +1745,7 @@
    1.56  "-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?";
    1.57  val t = TermC.str2term ("(1/x + 1/y + 1/z)  /  (1/x - 1/y - 1/z)  /  " ^
    1.58    "(2*x \<up> 2 / (x \<up> 2 - z \<up> 2) / (x / (x + z)  +  x / (x - z)))");
    1.59 -(* Rewrite.trace_on := true;
    1.60 +(* Rewrite.trace_on := true; (*true false*)
    1.61  rewrite_set_ thy false norm_Rational t;
    1.62  :
    1.63  ####  rls: cancel_p on: (2 * (x \<up> 6 * (y \<up> 2 * z)) + 2 * (x \<up> 6 * (y * z \<up> 2)) +