more standard declaration for presburger
authorhaftmann
Mon Oct 20 07:57:33 2014 +0200 (2014-10-20)
changeset 587113f7886cd75b9
parent 58710 7216a10d69ba
child 58712 709d8f68ec29
more standard declaration for presburger
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Mon Oct 20 07:45:58 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Mon Oct 20 07:57:33 2014 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4  
     1.5  definition even :: "'a \<Rightarrow> bool"
     1.6  where
     1.7 -  [algebra]: "even a \<longleftrightarrow> 2 dvd a"
     1.8 +  [presburger, algebra]: "even a \<longleftrightarrow> 2 dvd a"
     1.9  
    1.10  abbreviation odd :: "'a \<Rightarrow> bool"
    1.11  where
    1.12 @@ -298,7 +298,7 @@
    1.13    with False show ?thesis by auto
    1.14  qed
    1.15  
    1.16 -lemma even_iff_mod_2_eq_zero [presburger]:
    1.17 +lemma even_iff_mod_2_eq_zero:
    1.18    "even a \<longleftrightarrow> a mod 2 = 0"
    1.19    by (simp add: even_def dvd_eq_mod_eq_0)
    1.20