1.1 --- a/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Real.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -970,13 +970,6 @@
     1.4  qed
     1.5  end
     1.6  
     1.7 -text {*
     1.8 -  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
     1.9 -*}
    1.10 -
    1.11 -lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
    1.12 -  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
    1.13 -
    1.14  
    1.15  subsection {* Hiding implementation details *}
    1.16