1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Sat Jul 17 14:05:28 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Sun Jul 18 16:20:32 2021 +0200
     1.3 @@ -295,7 +295,7 @@
     1.4  (writeln o UnparseC.term) t;
     1.5  if UnparseC.term t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L \<up> 2) / 2)"
     1.6  then () else error "rewrite.sml rewrite_inst_ bdvs";
     1.7 -> Rewrite.trace_on:=true;
     1.8 +> Rewrite.trace_on:=true;false
     1.9  Rewrite.trace_on:=false;--------------------------------------------*)
    1.10  
    1.11  
    1.12 @@ -396,9 +396,9 @@
    1.13                            Const ("HOL.True", _))) => ()
    1.14    | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
    1.15  
    1.16 -tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
    1.17 +tracing "----- begin rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
    1.18  val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
    1.19 -tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false;
    1.20 +tracing "----- end rewrite x \<up> 2 * x ---"; Rewrite.trace_on := false; (*true false*)
    1.21  if UnparseC.term t' = "x * x \<up> 2" then ()
    1.22  else error "rewrite.sml Poly.is_multUnordered doesn't work";
    1.23  
    1.24 @@ -629,7 +629,7 @@
    1.25  
    1.26             rewrite__set_ thy (i + 1) false bdv rls a (*of*);
    1.27  
    1.28 -(*+*)Rewrite.trace_on := false;
    1.29 +(*+*)Rewrite.trace_on := false; (*true false*)
    1.30  
    1.31          (*this was False; vvvv--- means: indeterminate*)
    1.32      val (* SOME (t, a') *)NONE = (*case*)
    1.33 @@ -650,7 +650,7 @@
    1.34   :                             
    1.35   ###  asms accepted: [x \<noteq> 0]   stored: []
    1.36   : *)
    1.37 -Rewrite.trace_on := false;
    1.38 +Rewrite.trace_on := false; (*true false*)
    1.39  ( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
    1.40  
    1.41