1.1 --- a/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 09:26:11 2011 -0700
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Sat Sep 03 11:10:38 2011 -0700
     1.3 @@ -421,16 +421,6 @@
     1.4    assume allx': "ALL x. P x \<longrightarrow> x < z"
     1.5    have "EX s. ALL y. (EX x : Collect P. y < x) = (y < s)"
     1.6    proof (rule posreal_complete)
     1.7 -    show "ALL x : Collect P. 0 < x"
     1.8 -    proof safe
     1.9 -      fix x
    1.10 -      assume P: "P x"
    1.11 -      from allx
    1.12 -      have "P x \<longrightarrow> 0 < x"
    1.13 -        ..
    1.14 -      with P show "0 < x" by simp
    1.15 -    qed
    1.16 -  next
    1.17      from px
    1.18      show "EX x. x : Collect P"
    1.19        by auto

     2.1 --- a/src/HOL/RComplete.thy	Sat Sep 03 09:26:11 2011 -0700
     2.2 +++ b/src/HOL/RComplete.thy	Sat Sep 03 11:10:38 2011 -0700
     2.3 @@ -33,8 +33,8 @@
     2.4  text {* Only used in HOL/Import/HOL4Compat.thy; delete? *}
     2.5  
     2.6  lemma posreal_complete:
     2.7 -  assumes positive_P: "\<forall>x \<in> P. (0::real) < x"
     2.8 -    and not_empty_P: "\<exists>x. x \<in> P"
     2.9 +  fixes P :: "real set"
    2.10 +  assumes not_empty_P: "\<exists>x. x \<in> P"
    2.11      and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y"
    2.12    shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)"
    2.13  proof -