# HG changeset patch
# User huffman
# Date 1315073438 25200
# Node ID b6d8b11ed399b8f574e8b5c02fce95bc3403d506
# Parent  49ef76b4a63491f2952f420e226225d10eb5e920
remove unused assumption from lemma posreal_complete

diff -r 49ef76b4a634 -r b6d8b11ed399 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 09:26:11 2011 -0700
+++ b/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 11:10:38 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 49ef76b4a634 -r b6d8b11ed399 src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Sat Sep 03 09:26:11 2011 -0700
+++ b/src/HOL/RComplete.thy	Sat Sep 03 11:10:38 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 -