# HG changeset patch
# User huffman
# Date 1315085625 25200
# Node ID 42a2e1a4f04fdac01d44ddb5334c9c661ae4c941
# Parent  b6d8b11ed399b8f574e8b5c02fce95bc3403d506# Parent  e5ba1c0b8cac8eec430a58b1a5020284e91e361a
merged

diff -r e5ba1c0b8cac -r 42a2e1a4f04f src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 22:11:49 2011 +0200
+++ b/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 14:33:45 2011 -0700
@@ -421,16 +421,6 @@
   assume allx': "ALL x. P x \<longrightarrow> x < z"
   have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
   proof (rule posreal_complete)
-    show "ALL x : Collect P. 0 < x"
-    proof safe
-      fix x
-      assume P: "P x"
-      from allx
-      have "P x \<longrightarrow> 0 < x"
-        ..
-      with P show "0 < x" by simp
-    qed
-  next
     from px
     show "EX x. x : Collect P"
       by auto
diff -r e5ba1c0b8cac -r 42a2e1a4f04f src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Sat Sep 03 22:11:49 2011 +0200
+++ b/src/HOL/RComplete.thy	Sat Sep 03 14:33:45 2011 -0700
@@ -33,8 +33,8 @@
 text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
 
 lemma posreal_complete:
-  assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
-    and not_empty_P: "\<exists>x. x \<in> P"
+  fixes P :: "real set"
+  assumes not_empty_P: "\<exists>x. x \<in> P"
     and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
   shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
 proof -