# HG changeset patch
# User haftmann
# Date 1413784653 -7200
# Node ID 3f7886cd75b94319d40359272998dcfe4873ee42
# Parent  7216a10d69ba807cfcb972cbf230b093072e581a
more standard declaration for presburger

diff -r 7216a10d69ba -r 3f7886cd75b9 src/HOL/Parity.thy
--- 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)