1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri May 08 15:43:15 2015 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri May 08 16:03:38 2015 +0200
     1.3 @@ -78,13 +78,13 @@
     1.4  val od = ord_make_polynomial true (@{theory "Poly"});
     1.5  val t = str2term "((a + d) + c) + b";
     1.6  "((a + d) + c) + b"; 
     1.7 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
     1.8 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
     1.9  "b + ((a + d) + c)";
    1.10 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;
    1.11 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t; term2str t;
    1.12  "b + (c + (a + d))";
    1.13 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    1.14 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.15  "b + (a + (c + d))";
    1.16 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    1.17 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.18  "a + (b + (c + d))";
    1.19  if term2str t = "a + (b + (c + d))" then ()
    1.20  else error "polyminus.sml 2 watch order_add_mult";
    1.21 @@ -92,11 +92,11 @@
    1.22  "----- if parentheses are right, left_commute is (almost) sufficient...";
    1.23  val t = str2term "a + (d + (c + b))";
    1.24  "a + (d + (c + b))";
    1.25 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    1.26 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.27  "a + (c + (d + b))";
    1.28 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t;term2str t;
    1.29 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.commute} t;term2str t;
    1.30  "a + (c + (b + d))";
    1.31 -val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;
    1.32 +val SOME (t,_) = rewrite_ thy od e_rls true @{thm add.left_commute} t;term2str t;
    1.33  "a + (b + (c + d))";
    1.34  
    1.35  "----- but we do not want the parentheses at right; thus: cond.rew.";
    1.36 @@ -109,8 +109,8 @@
    1.37  "----- here we see rew_sub going into subterm with ord.rew....";
    1.38  val od = ord_make_polynomial false (@{theory "Poly"});
    1.39  val t = str2term "b + a + c + d";
    1.40 -val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
    1.41 -val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;
    1.42 +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
    1.43 +val SOME (t,_) = rewrite_ thy od e_rls false @{thm add.commute} t; term2str t;
    1.44  (*@@@ rew_sub gosub: t = d + (b + a + c)
    1.45    @@@ rew_sub begin: t = b + a + c*)
    1.46