author | huffman |
Tue, 11 May 2010 19:00:32 -0700 | |
changeset 36840 | 1e020f445846 |
parent 36839 | 34dc65df7014 |
child 36841 | 02df88789641 |
--- 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