src/HOL/Presburger.thy
changeset 31790 05c92381363c
parent 30686 47a32dd1b86e
child 32553 bf781ef40c81
     1.1 --- a/src/HOL/Presburger.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -399,7 +399,6 @@
     1.4  lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
     1.5  by simp
     1.6  lemma number_of2: "(0::int) <= Numeral0" by simp
     1.7 -lemma Suc_plus1: "Suc n = n + 1" by simp
     1.8  
     1.9  text {*
    1.10    \medskip Specific instances of congruence rules, to prevent