src/HOL/Presburger.thy
changeset 36749 a8dc19a352e6
parent 35216 7641e8d831d2
child 36798 3981db162131
     1.1 --- a/src/HOL/Presburger.thy	Thu May 06 23:37:07 2010 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Fri May 07 09:51:55 2010 +0200
     1.3 @@ -457,14 +457,4 @@
     1.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     1.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     1.6  
     1.7 -
     1.8 -lemma zdvd_period:
     1.9 -  fixes a d :: int
    1.10 -  assumes advdd: "a dvd d"
    1.11 -  shows "a dvd (x + t) \<longleftrightarrow> a dvd ((x + c * d) + t)"
    1.12 -  using advdd
    1.13 -  apply -
    1.14 -  apply (rule iffI)
    1.15 -  by algebra+
    1.16 -
    1.17  end