src/HOL/Presburger.thy
changeset 20217 25b068a99d2b
parent 20051 859e7129961b
child 20485 3078fd2eec7b
     1.1 --- a/src/HOL/Presburger.thy	Wed Jul 26 13:31:07 2006 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Jul 26 19:23:04 2006 +0200
     1.3 @@ -558,17 +558,13 @@
     1.4  lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
     1.5  apply(induct rule: int_gr_induct)
     1.6   apply simp
     1.7 - apply arith
     1.8  apply (simp add:int_distrib)
     1.9 -apply arith
    1.10  done
    1.11  
    1.12  lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
    1.13  apply(induct rule: int_gr_induct)
    1.14   apply simp
    1.15 - apply arith
    1.16  apply (simp add:int_distrib)
    1.17 -apply arith
    1.18  done
    1.19  
    1.20  lemma  minusinfinity: