src/HOL/Nat.ML
changeset 13438 527811f00c56
parent 13094 643fce75f6cd
child 13450 17fec4798b91
     1.1 --- a/src/HOL/Nat.ML	Wed Jul 31 14:40:40 2002 +0200
     1.2 +++ b/src/HOL/Nat.ML	Wed Jul 31 16:10:24 2002 +0200
     1.3 @@ -195,9 +195,8 @@
     1.4  qed "add_commute";
     1.5  
     1.6  Goal "x+(y+z)=y+((x+z)::nat)";
     1.7 -by (rtac (add_commute RS trans) 1);
     1.8 -by (rtac (add_assoc RS trans) 1);
     1.9 -by (rtac (add_commute RS arg_cong) 1);
    1.10 +by(rtac ([add_assoc,add_commute] MRS
    1.11 +         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
    1.12  qed "add_left_commute";
    1.13  
    1.14  (*Addition is an AC-operator*)
    1.15 @@ -426,11 +425,8 @@
    1.16  qed "mult_assoc";
    1.17  
    1.18  Goal "x*(y*z) = y*((x*z)::nat)";
    1.19 -by (rtac trans 1);
    1.20 -by (rtac mult_commute 1);
    1.21 -by (rtac trans 1);
    1.22 -by (rtac mult_assoc 1);
    1.23 -by (rtac (mult_commute RS arg_cong) 1);
    1.24 +by(rtac ([mult_assoc,mult_commute] MRS
    1.25 +         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
    1.26  qed "mult_left_commute";
    1.27  
    1.28  bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);