1.1 --- a/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Fri May 08 15:43:15 2015 +0200
     1.2 +++ b/test/Tools/isac/ADDTESTS/course/phst11/T2_Rewriting.thy	Fri May 08 16:03:38 2015 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  text {* That is fine, we just need to add 2+4 !!!!! See the next section below.
     1.5  
     1.6    But we cannot automate such ordering with what we know so far: If we put
     1.7 -  add_assoc, add_left_commute and add_commute into one ruleset (your have used
     1.8 +  add.assoc, add.left_commute and add.commute into one ruleset (your have used
     1.9    ruleset 'make_polynomial' already), then all the rules are applied as long
    1.10    as one rule is applicable (that is the way such rulesets work).
    1.11    Try to step through the ML-sections without skipping one of them ...

     2.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Fri May 08 15:43:15 2015 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Fri May 08 16:03:38 2015 +0200
     2.3 @@ -118,7 +118,7 @@
     2.4  "----------- rewrite-order ord_simplify_System -------------------";
     2.5  "----------- rewrite-order ord_simplify_System -------------------";
     2.6  "M_b x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
     2.7 -"--- add_commute ---";
     2.8 +"--- add.commute ---"; (* ... add_commute cf. b42e334c97ee *)
     2.9  if ord_simplify_System false thy [] (str2term"-1 * q_0 * (x ^^^ 2 / 2)", 
    2.10  				       str2term"c * x") then ()
    2.11  else error "integrate.sml, (-1 * q_0 * (x ^^^ 2 / 2)) < (c * x) not#1";

     3.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri May 08 15:43:15 2015 +0200
     3.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri May 08 16:03:38 2015 +0200
     3.3 @@ -78,13 +78,13 @@
     3.4  val od = ord_make_polynomial true (@{theory "Poly"});
     3.5  val t = str2term "((a + d) + c) + b";
     3.6  "((a + d) + c) + b"; 
     3.7 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
     3.8 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
     3.9  "b + ((a + d) + c)";
    3.10 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
    3.11 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
    3.12  "b + (c + (a + d))";
    3.13 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    3.14 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    3.15  "b + (a + (c + d))";
    3.16 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    3.17 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    3.18  "a + (b + (c + d))";
    3.19  if term2str t = "a + (b + (c + d))" then ()
    3.20  else error "polyminus.sml 2 watch order_add_mult";
    3.21 @@ -92,11 +92,11 @@
    3.22  "----- if parentheses are right, left_commute is (almost) sufficient...";
    3.23  val t = str2term "a + (d + (c + b))";
    3.24  "a + (d + (c + b))";
    3.25 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    3.26 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    3.27  "a + (c + (d + b))";
    3.28 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t;term2str t;
    3.29 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t;term2str t;
    3.30  "a + (c + (b + d))";
    3.31 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    3.32 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    3.33  "a + (b + (c + d))";
    3.34  
    3.35  "----- but we do not want the parentheses at right; thus: cond.rew.";
    3.36 @@ -109,8 +109,8 @@
    3.37  "----- here we see rew_sub going into subterm with ord.rew....";
    3.38  val od = ord_make_polynomial false (@{theory "Poly"});
    3.39  val t = str2term "b + a + c + d";
    3.40 -val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
    3.41 -val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
    3.42 +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
    3.43 +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
    3.44  (*@@@ rew_sub gosub: t = d + (b + a + c)
    3.45    @@@ rew_sub begin: t = b + a + c*)
    3.46