1.1 --- a/src/HOL/Presburger.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/Presburger.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -385,20 +385,6 @@
     1.4  
     1.5  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
     1.6  
     1.7 -lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
     1.8 -  by (simp split add: split_nat)
     1.9 -
    1.10 -lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
    1.11 -proof
    1.12 -  assume "\<exists>x. P x"
    1.13 -  then obtain x where "P x" ..
    1.14 -  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
    1.15 -  then show "\<exists>x\<ge>0. P (nat x)" ..
    1.16 -next
    1.17 -  assume "\<exists>x\<ge>0. P (nat x)"
    1.18 -  then show "\<exists>x. P x" by auto
    1.19 -qed
    1.20 -
    1.21  lemma zdiff_int_split: "P (int (x - y)) =
    1.22    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"
    1.23    by (case_tac "y \<le> x", simp_all add: zdiff_int)