--- a/src/HOL/Parity.thy Mon Oct 20 07:45:58 2014 +0200
+++ b/src/HOL/Parity.thy Mon Oct 20 07:57:33 2014 +0200
@@ -191,7 +191,7 @@
definition even :: "'a \<Rightarrow> bool"
where
- [algebra]: "even a \<longleftrightarrow> 2 dvd a"
+ [presburger, algebra]: "even a \<longleftrightarrow> 2 dvd a"
abbreviation odd :: "'a \<Rightarrow> bool"
where
@@ -298,7 +298,7 @@
with False show ?thesis by auto
qed
-lemma even_iff_mod_2_eq_zero [presburger]:
+lemma even_iff_mod_2_eq_zero:
"even a \<longleftrightarrow> a mod 2 = 0"
by (simp add: even_def dvd_eq_mod_eq_0)