1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Sat Jul 17 14:05:28 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Sun Jul 18 16:20:32 2021 +0200
     1.3 @@ -164,12 +164,12 @@
     1.4  "----------- watch order_add_mult  -------------------------------";
     1.5  "----- with these simple variables it works...";
     1.6  (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
     1.7 -Rewrite.trace_on:=false;
     1.8 +Rewrite.trace_on:=false; (*true false*)
     1.9  val t = TermC.str2term "((a + d) + c) + b";
    1.10  val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
    1.11  if UnparseC.term t = "a + (b + (c + d))" then ()
    1.12  else error "polyminus.sml 1 watch order_add_mult";
    1.13 -Rewrite.trace_on:=false;
    1.14 +Rewrite.trace_on:=false; (*true false*)
    1.15  
    1.16  "----- the same stepwise...";
    1.17  val od = ord_make_polynomial true (@{theory "Poly"});
    1.18 @@ -325,7 +325,7 @@
    1.19  else error "polyminus.sml: verschoenere 3 + - 2 * e ...";
    1.20  
    1.21  (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
    1.22 -Rewrite.trace_on:=false;
    1.23 +Rewrite.trace_on:=false; (*true false*)
    1.24  
    1.25  "----------- met simplification for_polynomials with_minus -------";
    1.26  "----------- met simplification for_polynomials with_minus -------";
    1.27 @@ -538,7 +538,7 @@
    1.28  val SOME (t',_) = 
    1.29      rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
    1.30  UnparseC.term t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
    1.31 -Rewrite.trace_on := false;
    1.32 +Rewrite.trace_on := false; (*true false*)
    1.33  
    1.34  
    1.35  applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
    1.36 @@ -684,7 +684,7 @@
    1.37  	      (*"(~ False) = True"*)];
    1.38  (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
    1.39  val SOME (t', _) = rewrite_set_ thy false prls t;
    1.40 -Rewrite.trace_on := false;
    1.41 +Rewrite.trace_on := false; (*true false*)
    1.42  
    1.43  "--- does the respective prls rewrite the whole predicate ?";
    1.44  val t = TermC.str2term 
    1.45 @@ -694,7 +694,7 @@
    1.46  	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
    1.47  (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
    1.48  val SOME (t', _) = rewrite_set_ thy false prls t;
    1.49 -Rewrite.trace_on := false;
    1.50 +Rewrite.trace_on := false; (*true false*)
    1.51  if UnparseC.term t' = "False" then ()
    1.52  else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
    1.53