src/HOL/Parity.thy
changeset 36840 1e020f445846
parent 36722 c8ea75ea4a29
child 41959 b460124855b8
     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