--- a/src/HOL/Presburger.thy Thu Feb 18 13:29:59 2010 -0800
+++ b/src/HOL/Presburger.thy Thu Feb 18 14:21:44 2010 -0800
@@ -199,16 +199,16 @@
hence "P 0" using P Pmod by simp
moreover have "P 0 = P(0 - (-1)*d)" using modd by blast
ultimately have "P d" by simp
- moreover have "d : {1..d}" using dpos by(simp add:atLeastAtMost_iff)
+ moreover have "d : {1..d}" using dpos by simp
ultimately show ?RHS ..
next
assume not0: "x mod d \<noteq> 0"
- have "P(x mod d)" using dpos P Pmod by(simp add:pos_mod_sign pos_mod_bound)
+ have "P(x mod d)" using dpos P Pmod by simp
moreover have "x mod d : {1..d}"
proof -
from dpos have "0 \<le> x mod d" by(rule pos_mod_sign)
moreover from dpos have "x mod d < d" by(rule pos_mod_bound)
- ultimately show ?thesis using not0 by(simp add:atLeastAtMost_iff)
+ ultimately show ?thesis using not0 by simp
qed
ultimately show ?RHS ..
qed