src/HOL/Library/Pocklington.thy

--- a/src/HOL/Library/Pocklington.thy	Mon May 18 09:48:06 2009 +0200
+++ b/src/HOL/Library/Pocklington.thy	Mon May 18 23:15:38 2009 +0200
@@ -382,8 +382,9 @@
 (* Euler totient function.                                                   *)
 
 definition phi_def: "\<phi> n = card { m. 0 < m \<and> m <= n \<and> coprime m n }"
+
 lemma phi_0[simp]: "\<phi> 0 = 0"
-  unfolding phi_def by (auto simp add: card_eq_0_iff)
+  unfolding phi_def by auto
 
 lemma phi_finite[simp]: "finite ({ m. 0 < m \<and> m <= n \<and> coprime m n })"
 proof-