merged
authorhuffman
Sat, 03 Sep 2011 14:33:45 -0700
changeset 44691 42a2e1a4f04f
parent 44690 b6d8b11ed399 (diff)
parent 44682 e5ba1c0b8cac (current diff)
child 44692 ccfc7c193d2b
merged
--- 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 -