1.1 --- a/src/HOL/IntDiv.thy	Wed Sep 09 12:29:06 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Sep 10 14:07:58 2009 +0200
     1.3 @@ -1102,20 +1102,6 @@
     1.4    thus ?thesis by simp
     1.5  qed
     1.6  
     1.7 -
     1.8 -theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
     1.9 -apply (simp split add: split_nat)
    1.10 -apply (rule iffI)
    1.11 -apply (erule exE)
    1.12 -apply (rule_tac x = "int x" in exI)
    1.13 -apply simp
    1.14 -apply (erule exE)
    1.15 -apply (rule_tac x = "nat x" in exI)
    1.16 -apply (erule conjE)
    1.17 -apply (erule_tac x = "nat x" in allE)
    1.18 -apply simp
    1.19 -done
    1.20 -
    1.21  theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    1.22  proof -
    1.23    have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"