src/HOL/RComplete.thy
changeset 44669 8e6cdb9c00a7
parent 44668 31d41a0f6b5d
child 44678 21eb31192850
     1.1 --- a/src/HOL/RComplete.thy	Fri Sep 02 15:19:59 2011 -0700
     1.2 +++ b/src/HOL/RComplete.thy	Fri Sep 02 16:48:30 2011 -0700
     1.3 @@ -80,14 +80,6 @@
     1.4        Collect_def mem_def isUb_def UNIV_def by simp
     1.5  qed
     1.6  
     1.7 -text{*A version of the same theorem without all those predicates!*}
     1.8 -lemma reals_complete2:
     1.9 -  fixes S :: "(real set)"
    1.10 -  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
    1.11 -  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
    1.12 -               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
    1.13 -using assms by (rule complete_real)
    1.14 -
    1.15  
    1.16  subsection {* The Archimedean Property of the Reals *}
    1.17