diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Real.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -970,13 +970,6 @@
 qed
 end
 
-text {*
-  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
-*}
-
-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"
-  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
-
 
 subsection {* Hiding implementation details *}