diff -r a03462cbf86f -r 7641e8d831d2 src/HOL/Presburger.thy
--- 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