test/Tools/isac/OLDTESTS/root-equ.sml
changeset 59900 4e6fc3336336
parent 59881 bdced24f62bf
child 59901 07a042166900
     1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Apr 21 16:16:11 2020 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Tue Apr 21 16:53:17 2020 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4 -(* trace_rewrite:= true;
     1.5 -   trace_rewrite:= false;
     1.6 +(* Trace.trace_rewrite:= true;
     1.7 +   Trace.trace_rewrite:= false;
     1.8  
     1.9     method "sqrt-equ-test", _NOT_ "square-equation" 
    1.10  *)
    1.11 @@ -546,8 +546,8 @@
    1.12   val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
    1.13   val SOME (t',asm) = rewrite_set_ thy false rls t;
    1.14   UnparseC.term t';
    1.15 -> trace_rewrite:=true; 
    1.16 - trace_rewrite:=false; 
    1.17 +> Trace.trace_rewrite:=true; 
    1.18 + Trace.trace_rewrite:=false; 
    1.19  *)
    1.20  
    1.21  (*me------------