src/HOL/Parity.thy

--- a/src/HOL/Parity.thy	Tue May 11 18:06:58 2010 -0700
+++ b/src/HOL/Parity.thy	Tue May 11 19:00:32 2010 -0700
@@ -61,7 +61,7 @@
 subsection {* Behavior under integer arithmetic operations *}
 declare dvd_def[algebra]
 lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \<longleftrightarrow> 2 dvd x"
-  by (presburger add: even_nat_def even_def)
+  by presburger
 lemma int_even_iff_2_dvd[algebra]: "even (x::int) \<longleftrightarrow> 2 dvd x"
   by presburger