# HG changeset patch
# User huffman
# Date 1273629632 25200
# Node ID 1e020f4458464a0368e34b4a5e944b95a39f3390
# Parent  34dc65df701421fe4cb78aad9087f38f3baa1dbc
fix duplicate simp rule warning

diff -r 34dc65df7014 -r 1e020f445846 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