src/Tools/isac/Build_Isac.thy
changeset 60503 822fdba88dfc
parent 60502 474a00f8b91e
child 60507 b125dcf14489
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Jul 31 13:23:38 2022 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Sun Jul 31 13:45:20 2022 +0200
     1.3 @@ -202,14 +202,6 @@
     1.4  text \<open>
     1.5    REPLACE BY Know_Store... (has been overlooked)
     1.6      calcelems.sml:val rew_ord' = Unsynchronized.ref ...
     1.7 -  KEEP FOR TRACING
     1.8 -    rewrite.sml:val Rewrite.trace_on = Unsynchronized.ref false;
     1.9 -    rewrite.sml:val depth = Unsynchronized.ref 99999;
    1.10 -    rewrite.sml:val lim_rewrite = Unsynchronized.ref 99999;
    1.11 -    rewrite.sml:val lim_deriv = Unsynchronized.ref 100;
    1.12 -    Interpret/rewtools.sml:val LItool.trace = Unsynchronized.ref false;
    1.13 -  KEEP FOR EASIER DEVELOPMENT
    1.14 -    calcelems.sml:val check_guhs_unique = Unsynchronized.ref true;
    1.15    KEEP FOR DEMOS
    1.16      Knowledge/GCD_Poly_ML.thy:  val trace_div = Unsynchronized.ref true;
    1.17      Knowledge/GCD_Poly_ML.thy:  val trace_div_invariant = Unsynchronized.ref false;