src/HOL/Presburger.thy
changeset 35216 7641e8d831d2
parent 35050 9f841f20dca6
child 36749 a8dc19a352e6
     1.1 --- a/src/HOL/Presburger.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Presburger.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -199,16 +199,16 @@
     1.4      hence "P 0" using P Pmod by simp
     1.5      moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
     1.6      ultimately have "P d" by simp
     1.7 -    moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
     1.8 +    moreover have "d : {1..d}" using dpos by simp
     1.9      ultimately show ?RHS ..
    1.10    next
    1.11      assume not0: "x mod d \<noteq> 0"
    1.12 -    have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
    1.13 +    have "P(x mod d)" using dpos P Pmod by simp
    1.14      moreover have "x mod d : {1..d}"
    1.15      proof -
    1.16        from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
    1.17        moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
    1.18 -      ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
    1.19 +      ultimately show ?thesis using not0 by simp
    1.20      qed
    1.21      ultimately show ?RHS ..
    1.22    qed