1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Sat Jul 17 14:05:28 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Sun Jul 18 16:20:32 2021 +0200
     1.3 @@ -49,9 +49,8 @@
     1.4  "----------- tests on predicates in problems ---------------------";
     1.5  "----------- tests on predicates in problems ---------------------";
     1.6  "----------- tests on predicates in problems ---------------------";
     1.7 -(* Rewrite.trace_on:=true;
     1.8 - Rewrite.trace_on:=false;
     1.9 -*)
    1.10 +Rewrite.trace_on:=true;  (*true false*)
    1.11 +
    1.12   val t1 = (Thm.term_of o the o (TermC.parse thy)) "lhs (-8 - 2*x + x \<up> 2 = 0)";
    1.13   val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
    1.14   if ((UnparseC.term t) = "-8 - 2 * x + x \<up> 2") then ()
    1.15 @@ -160,7 +159,7 @@
    1.16    "x \<up> 2 + (- 1 * (b * x)) + (b + - 1 * x) * a = 0"*)
    1.17  
    1.18    (*das rewriting l"asst sich beobachten mit
    1.19 -Rewrite.trace_on := false;
    1.20 +Rewrite.trace_on := false; (*true false*)
    1.21    *)
    1.22  
    1.23  "------ 15.11.02 --------------------------";
    1.24 @@ -168,7 +167,7 @@
    1.25    val bdv = (Thm.term_of o the o (TermC.parse thy)) "bdv";
    1.26    val a = (Thm.term_of o the o (TermC.parse thy)) "a";
    1.27   
    1.28 -Rewrite.trace_on := false;
    1.29 +Rewrite.trace_on := false; (*true false*)
    1.30   (* Anwenden einer Regelmenge aus Termorder.ML: *)
    1.31   val SOME (t,_) =
    1.32       rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;