diff -r 628fe06cbeff -r 59b50c691b75 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Mon May 10 14:11:50 2010 +0200 +++ b/src/HOL/Presburger.thy Mon May 10 14:18:41 2010 +0200 @@ -15,7 +15,6 @@ subsection{* The @{text "-\"} and @{text "+\"} Properties *} - lemma minf: "\\(z ::'a::linorder).\xz.\x \ \z.\x Q x) = (P' x \ Q' x)" @@ -384,10 +383,11 @@ lemma zdiff_int_split: "P (int (x - y)) = ((y \ x \ P (int x - int y)) \ (x < y \ P 0))" - by (case_tac "y \ x", simp_all add: zdiff_int) + by (cases "y \ x") (simp_all add: zdiff_int) lemma number_of1: "(0::int) <= number_of n \ (0::int) <= number_of (Int.Bit0 n) \ (0::int) <= number_of (Int.Bit1 n)" by simp + lemma number_of2: "(0::int) <= Numeral0" by simp text {* @@ -399,10 +399,6 @@ theorem conj_le_cong: "(0 <= x \ P = P') \ (0 <= (x::int) \ P) = (0 <= x \ P')" by (simp cong: conj_cong) -lemma int_eq_number_of_eq: - "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)" - by (rule eq_number_of_eq) - use "Tools/Qelim/cooper.ML" setup Cooper.setup