fix duplicate simp rule warning
authorhuffman
Tue May 11 19:00:32 2010 -0700 (2010-05-11)
changeset 368401e020f445846
parent 36839 34dc65df7014
child 36841 02df88789641
fix duplicate simp rule warning
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Tue May 11 18:06:58 2010 -0700
     1.2 +++ b/src/HOL/Parity.thy	Tue May 11 19:00:32 2010 -0700
     1.3 @@ -61,7 +61,7 @@
     1.4  subsection {* Behavior under integer arithmetic operations *}
     1.5  declare dvd_def[algebra]
     1.6  lemma nat_even_iff_2_dvd[algebra]: "even (x::nat) \<longleftrightarrow> 2 dvd x"
     1.7 -  by (presburger add: even_nat_def even_def)
     1.8 +  by presburger
     1.9  lemma int_even_iff_2_dvd[algebra]: "even (x::int) \<longleftrightarrow> 2 dvd x"
    1.10    by presburger
    1.11