changeset 31790 | 05c92381363c |
parent 30686 | 47a32dd1b86e |
child 32553 | bf781ef40c81 |
--- 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