--- a/src/HOL/Nat.thy Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Nat.thy Thu Feb 18 14:21:44 2010 -0800
@@ -1356,7 +1356,7 @@
end
lemma of_nat_id [simp]: "of_nat n = n"
- by (induct n) (auto simp add: One_nat_def)
+ by (induct n) simp_all
lemma of_nat_eq_id [simp]: "of_nat = id"
by (auto simp add: expand_fun_eq)
@@ -1619,7 +1619,7 @@
lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
unfolding dvd_def
- by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
+ by (force dest: mult_eq_self_implies_10 simp add: mult_assoc)
text {* @{term "op dvd"} is a partial order *}