1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Tue Apr 21 16:53:17 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Wed Apr 22 11:06:48 2020 +0200
1.3 @@ -66,13 +66,13 @@
1.4 "----------- watch order_add_mult -------------------------------";
1.5 "----------- watch order_add_mult -------------------------------";
1.6 "----- with these simple variables it works...";
1.7 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
1.8 -Trace.trace_rewrite:=false;
1.9 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.10 +Rewrite.trace_on:=false;
1.11 val t = str2term "((a + d) + c) + b";
1.12 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; UnparseC.term t;
1.13 if UnparseC.term t = "a + (b + (c + d))" then ()
1.14 else error "polyminus.sml 1 watch order_add_mult";
1.15 -Trace.trace_rewrite:=false;
1.16 +Rewrite.trace_on:=false;
1.17
1.18 "----- the same stepwise...";
1.19 val od = ord_make_polynomial true (@{theory "Poly"});
1.20 @@ -169,7 +169,7 @@
1.21 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; UnparseC.term t;
1.22
1.23 "======= test rewrite_, rewrite_set_";
1.24 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
1.25 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.26 val erls = erls_ordne_alphabetisch;
1.27 val t = str2term "b + a";
1.28 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; UnparseC.term t;
1.29 @@ -227,8 +227,8 @@
1.30 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then ()
1.31 else error "polyminus.sml: verschoenere 3 + -2 * e ...";
1.32
1.33 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
1.34 -Trace.trace_rewrite:=false;
1.35 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.36 +Rewrite.trace_on:=false;
1.37
1.38 "----------- met simplification for_polynomials with_minus -------";
1.39 "----------- met simplification for_polynomials with_minus -------";
1.40 @@ -420,7 +420,7 @@
1.41 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
1.42 val ((pt,p),_) = get_calc 1; show_pt pt;
1.43 "----- 2 ^^^";
1.44 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
1.45 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.46 val erls = erls_ordne_alphabetisch;
1.47 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
1.48 val SOME (t',_) =
1.49 @@ -435,7 +435,7 @@
1.50 val SOME (t',_) =
1.51 rewrite_set_ (@{theory "Isac_Knowledge"}) false ordne_alphabetisch t;
1.52 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";
1.53 -Trace.trace_rewrite := false;
1.54 +Rewrite.trace_on := false;
1.55
1.56
1.57 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
1.58 @@ -577,9 +577,9 @@
1.59 (*"(~ True) = False"*)
1.60 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.61 (*"(~ False) = True"*)];
1.62 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
1.63 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.64 val SOME (t', _) = rewrite_set_ thy false prls t;
1.65 -Trace.trace_rewrite := false;
1.66 +Rewrite.trace_on := false;
1.67
1.68 "--- does the respective prls rewrite the whole predicate ?";
1.69 val t = str2term
1.70 @@ -587,9 +587,9 @@
1.71 \ matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \
1.72 \ matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \
1.73 \ matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";
1.74 -(*Trace.trace_rewrite := true; ..stopped Test_Isac.thy*)
1.75 +(*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.76 val SOME (t', _) = rewrite_set_ thy false prls t;
1.77 -Trace.trace_rewrite := false;
1.78 +Rewrite.trace_on := false;
1.79 if UnparseC.term t' = "False" then ()
1.80 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";
1.81