fix duplicate simp rule warning
authorhuffman
Tue, 11 May 2010 19:00:32 -0700
changeset 36840 1e020f445846
parent 36839 34dc65df7014
child 36841 02df88789641
fix duplicate simp rule warning
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