# HG changeset patch
# User haftmann
# Date 1273493921 -7200
# Node ID 59b50c691b75665c02c5049a3bd62945e6a93d2f
# Parent  628fe06cbeffa96e0498eafe21d49591144c0e64
tuned theory text; dropped unused lemma

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 "-\<infinity>"} and @{text "+\<infinity>"} Properties *}
 
-
 lemma minf:
   "\<lbrakk>\<exists>(z ::'a::linorder).\<forall>x<z. P x = P' x; \<exists>z.\<forall>x<z. Q x = Q' x\<rbrakk> 
      \<Longrightarrow> \<exists>z.\<forall>x<z. (P x \<and> Q x) = (P' x \<and> Q' x)"
@@ -384,10 +383,11 @@
 
 lemma zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
-  by (case_tac "y \<le> x", simp_all add: zdiff_int)
+  by (cases "y \<le> x") (simp_all add: zdiff_int)
 
 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
 
 text {*
@@ -399,10 +399,6 @@
 theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> 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