# HG changeset patch
# User Walther Neuper <wneuper@ist.tugraz.at>
# Date 1431093818 -7200
# Node ID 5a0e75dec74995a759d36fb0692c7c8b6526b8e2
# Parent  e92d1e6a3497e7bfcb3c212457dd6518e2735497
Isabelle201302 --> Isabelle2014: add.commute cf. b42e334c97ee

diff -r e92d1e6a3497 -r 5a0e75dec749 test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy
--- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Fri May 08 15:43:15 2015 +0200
+++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Fri May 08 16:03:38 2015 +0200
@@ -110,7 +110,7 @@
 text {* That is fine, we just need to add 2+4 !!!!! See the next section below.
 
   But we cannot automate such ordering with what we know so far: If we put
-  add_assoc, add_left_commute and add_commute into one ruleset (your have used
+  add.assoc, add.left_commute and add.commute into one ruleset (your have used
   ruleset 'make_polynomial' already), then all the rules are applied as long
   as one rule is applicable (that is the way such rulesets work).
   Try to step through the ML-sections without skipping one of them ...
diff -r e92d1e6a3497 -r 5a0e75dec749 test/Tools/isac/Knowledge/eqsystem.sml
--- a/test/Tools/isac/Knowledge/eqsystem.sml	Fri May 08 15:43:15 2015 +0200
+++ b/test/Tools/isac/Knowledge/eqsystem.sml	Fri May 08 16:03:38 2015 +0200
@@ -118,7 +118,7 @@
 "----------- rewrite-order ord_simplify_System -------------------";
 "----------- rewrite-order ord_simplify_System -------------------";
 "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
-"--- add_commute ---";
+"--- add.commute ---"; (* ... add_commute cf. b42e334c97ee *)
 if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)", 
 				       str2term"c * x") then ()
 else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";
diff -r e92d1e6a3497 -r 5a0e75dec749 test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Fri May 08 15:43:15 2015 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri May 08 16:03:38 2015 +0200
@@ -78,13 +78,13 @@
 val od = ord_make_polynomial true (@{theory "Poly"});
 val t = str2term "((a + d) + c) + b";
 "((a + d) + c) + b"; 
-val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
 "b + ((a + d) + c)";
-val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
 "b + (c + (a + d))";
-val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
 "b + (a + (c + d))";
-val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
 "a + (b + (c + d))";
 if term2str t = "a + (b + (c + d))" then ()
 else error "polyminus.sml 2 watch order_add_mult";
@@ -92,11 +92,11 @@
 "----- if parentheses are right, left_commute is (almost) sufficient...";
 val t = str2term "a + (d + (c + b))";
 "a + (d + (c + b))";
-val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
 "a + (c + (d + b))";
-val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t;term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t;term2str t;
 "a + (c + (b + d))";
-val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
 "a + (b + (c + d))";
 
 "----- but we do not want the parentheses at right; thus: cond.rew.";
@@ -109,8 +109,8 @@
 "----- here we see rew_sub going into subterm with ord.rew....";
 val od = ord_make_polynomial false (@{theory "Poly"});
 val t = str2term "b + a + c + d";
-val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
-val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
+val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
 (*@@@ rew_sub gosub: t = d + (b + a + c)
   @@@ rew_sub begin: t = b + a + c*)