src/HOL/Nat.thy
changeset 35216 7641e8d831d2
parent 35121 36c0a6dd8c6f
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Nat.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Nat.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -1356,7 +1356,7 @@
     1.4  end
     1.5  
     1.6  lemma of_nat_id [simp]: "of_nat n = n"
     1.7 -  by (induct n) (auto simp add: One_nat_def)
     1.8 +  by (induct n) simp_all
     1.9  
    1.10  lemma of_nat_eq_id [simp]: "of_nat = id"
    1.11    by (auto simp add: expand_fun_eq)
    1.12 @@ -1619,7 +1619,7 @@
    1.13  
    1.14  lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
    1.15    unfolding dvd_def
    1.16 -  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
    1.17 +  by (force dest: mult_eq_self_implies_10 simp add: mult_assoc)
    1.18  
    1.19  text {* @{term "op dvd"} is a partial order *}
    1.20