src/HOL/Nat.thy

   unfolding abs_if by auto
 
 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)
 
 

 lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
 by (simp add: dvd_def)
 
 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 *}
 
 interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
   proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)