--- a/src/HOL/Nat.ML Wed Jul 31 14:40:40 2002 +0200
+++ b/src/HOL/Nat.ML Wed Jul 31 16:10:24 2002 +0200
@@ -195,9 +195,8 @@
qed "add_commute";
Goal "x+(y+z)=y+((x+z)::nat)";
-by (rtac (add_commute RS trans) 1);
-by (rtac (add_assoc RS trans) 1);
-by (rtac (add_commute RS arg_cong) 1);
+by(rtac ([add_assoc,add_commute] MRS
+ read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
qed "add_left_commute";
(*Addition is an AC-operator*)
@@ -426,11 +425,8 @@
qed "mult_assoc";
Goal "x*(y*z) = y*((x*z)::nat)";
-by (rtac trans 1);
-by (rtac mult_commute 1);
-by (rtac trans 1);
-by (rtac mult_assoc 1);
-by (rtac (mult_commute RS arg_cong) 1);
+by(rtac ([mult_assoc,mult_commute] MRS
+ read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
qed "mult_left_commute";
bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);