src/Tools/isac/Build_Isac.thy
changeset 59901 07a042166900
parent 59892 b8cfae027755
child 59902 e7910a62eaf2
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Tue Apr 21 16:53:17 2020 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Wed Apr 22 11:06:48 2020 +0200
     1.3 @@ -150,11 +150,11 @@
     1.4    REPLACE BY Know_Store... (has been overlooked)
     1.5      calcelems.sml:val rew_ord' = Unsynchronized.ref ...
     1.6    KEEP FOR TRACING
     1.7 -    calcelems.sml:val trace_rewrite = Unsynchronized.ref false;
     1.8 -    calcelems.sml:val depth = Unsynchronized.ref 99999;
     1.9 -    calcelems.sml:val lim_rewrite = Unsynchronized.ref 99999;
    1.10 -    calcelems.sml:val lim_deriv = Unsynchronized.ref 100;
    1.11 -    Interpret/script.sml:val trace_LI = Unsynchronized.ref false;
    1.12 +    rewrite.sml:val Rewrite.trace_on = Unsynchronized.ref false;
    1.13 +    rewrite.sml:val depth = Unsynchronized.ref 99999;
    1.14 +    rewrite.sml:val lim_rewrite = Unsynchronized.ref 99999;
    1.15 +    rewrite.sml:val lim_deriv = Unsynchronized.ref 100;
    1.16 +    Interpret/rewtools.sml:val LItool.trace = Unsynchronized.ref false;
    1.17    KEEP FOR EASIER DEVELOPMENT
    1.18      calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
    1.19    KEEP FOR DEMOS