diff -r c8a590599cb5 -r 05c92381363c src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Jun 23 21:07:39 2009 +0200
+++ b/src/HOL/Presburger.thy	Wed Jun 24 09:41:14 2009 +0200
@@ -399,7 +399,6 @@
 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
 by simp
 lemma number_of2: "(0::int) <= Numeral0" by simp
-lemma Suc_plus1: "Suc n = n + 1" by simp
 
 text {*
   \medskip Specific instances of congruence rules, to prevent