--- 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
--- 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 -