diff -r 1f3b832c90c1 -r f31794033ae1 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/Presburger.thy	Wed Jun 13 03:31:11 2007 +0200
@@ -383,29 +383,14 @@
   by (simp split add: split_nat)
 
 lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-  by (auto split add: split_nat) 
-(rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
+  apply (auto split add: split_nat)
+  apply (rule_tac x="int x" in exI, simp)
+  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
+  done
 
 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)
-
-lemma zdvd_int: "(x dvd y) = (int x dvd int y)"
-  apply (simp only: dvd_def ex_nat int_int_eq [symmetric] zmult_int [symmetric]
-    nat_0_le cong add: conj_cong)
-  apply (rule iffI)
-  apply iprover
-  apply (erule exE)
-  apply (case_tac "x=0")
-  apply (rule_tac x=0 in exI)
-  apply simp
-  apply (case_tac "0 \<le> k")
-  apply iprover
-  apply (simp add: linorder_not_le)
-  apply (drule mult_strict_left_mono_neg [OF iffD2 [OF zero_less_int_conv]])
-  apply assumption
-  apply (simp add: mult_ac)
-  done
+  by (case_tac "y \<le> x", simp_all)
 
 lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)" by simp
 lemma number_of2: "(0::int) <= Numeral0" by simp
@@ -670,4 +655,4 @@
   less_Bit0_Min less_Bit1_Min less_Bit_Bit0 less_Bit1_Bit less_Bit0_Bit1
   less_number_of
 
-end
\ No newline at end of file
+end