src/HOL/Nat.thy
changeset 57514 bdc2c6b40bf2
parent 57512 cc97b347b301
child 57952 1a9a6dfc255f
     1.1 --- a/src/HOL/Nat.thy	Sat Jul 05 10:09:01 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Jul 05 11:01:53 2014 +0200
     1.3 @@ -1075,10 +1075,10 @@
     1.4  lemma add_leE: "(m::nat) + k \<le> n ==> (m \<le> n ==> k \<le> n ==> R) ==> R"
     1.5  by (blast dest: add_leD1 add_leD2)
     1.6  
     1.7 -text {* needs @{text "!!k"} for @{text add_ac} to work *}
     1.8 +text {* needs @{text "!!k"} for @{text ac_simps} to work *}
     1.9  lemma less_add_eq_less: "!!k::nat. k < l ==> m + l = k + n ==> m < n"
    1.10  by (force simp del: add_Suc_right
    1.11 -    simp add: less_iff_Suc_add add_Suc_right [symmetric] add_ac)
    1.12 +    simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)
    1.13  
    1.14  
    1.15  subsubsection {* More results about difference *}
    1.16 @@ -1405,10 +1405,10 @@
    1.17    by (simp add: of_nat_def)
    1.18  
    1.19  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
    1.20 -  by (induct m) (simp_all add: add_ac)
    1.21 +  by (induct m) (simp_all add: ac_simps)
    1.22  
    1.23  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    1.24 -  by (induct m) (simp_all add: add_ac distrib_right)
    1.25 +  by (induct m) (simp_all add: ac_simps distrib_right)
    1.26  
    1.27  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
    1.28    "of_nat_aux inc 0 i = i"
    1.29 @@ -1869,7 +1869,7 @@
    1.30  lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
    1.31    unfolding dvd_def
    1.32    apply (erule exE)
    1.33 -  apply (simp add: mult_ac)
    1.34 +  apply (simp add: ac_simps)
    1.35    done
    1.36  
    1.37  lemma dvd_mult_cancel1: "0<m ==> (m*n dvd m) = (n = (1::nat))"