1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Apr 21 16:53:17 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Wed Apr 22 11:06:48 2020 +0200
1.3 @@ -49,8 +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 -(* Trace.trace_rewrite:=true;
1.8 - Trace.trace_rewrite:=false;
1.9 +(* Rewrite.trace_on:=true;
1.10 + Rewrite.trace_on:=false;
1.11 *)
1.12 val t1 = (Thm.term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
1.13 val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t1;
1.14 @@ -160,7 +160,7 @@
1.15 "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
1.16
1.17 (*das rewriting l"asst sich beobachten mit
1.18 -Trace.trace_rewrite := false;
1.19 +Rewrite.trace_on := false;
1.20 *)
1.21
1.22 "------15.11.02 --------------------------";
1.23 @@ -168,7 +168,7 @@
1.24 val bdv = (Thm.term_of o the o (parse thy)) "bdv";
1.25 val a = (Thm.term_of o the o (parse thy)) "a";
1.26
1.27 -Trace.trace_rewrite := false;
1.28 +Rewrite.trace_on := false;
1.29 (* Anwenden einer Regelmenge aus Termorder.ML: *)
1.30 val SOME (t,_) =
1.31 rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;