--- a/src/HOL/Presburger.thy Thu May 06 23:37:07 2010 +0200
+++ b/src/HOL/Presburger.thy Fri May 07 09:51:55 2010 +0200
@@ -457,14 +457,4 @@
lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
-
-lemma zdvd_period:
- fixes a d :: int
- assumes advdd: "a dvd d"
- shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
- using advdd
- apply -
- apply (rule iffI)
- by algebra+
-
end