diff -r 3406cd754dd2 -r e6928fc2332a src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jul 21 21:56:24 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 21 22:47:13 2011 +0200
@@ -1338,33 +1338,6 @@
     by (cases e) auto
 qed
 
-lemma (in complete_linorder) Sup_eq_top_iff: -- "FIXME move"
-  "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
-proof
-  assume *: "Sup A = top"
-  show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
-  proof (intro allI impI)
-    fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
-      unfolding less_Sup_iff by auto
-  qed
-next
-  assume *: "\<forall>x<top. \<exists>i\<in>A. x < i"
-  show "Sup A = top"
-  proof (rule ccontr)
-    assume "Sup A \<noteq> top"
-    with top_greatest [of "Sup A"]
-    have "Sup A < top" unfolding le_less by auto
-    then have "Sup A < Sup A"
-      using * unfolding less_Sup_iff by auto
-    then show False by auto
-  qed
-qed
-
-lemma (in complete_linorder) SUP_eq_top_iff: -- "FIXME move"
-  fixes f :: "'b \<Rightarrow> 'a"
-  shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
-  unfolding SUPR_def Sup_eq_top_iff by auto
-
 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
 proof -
   { fix x ::ereal assume "x \<noteq> \<infinity>"
@@ -2374,14 +2347,6 @@
 
 abbreviation "limsup \<equiv> Limsup sequentially"
 
-lemma (in complete_lattice) less_INFD:
-  assumes "y < INFI A f"" i \<in> A" shows "y < f i"
-proof -
-  note `y < INFI A f`
-  also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI)
-  finally show "y < f i" .
-qed
-
 lemma liminf_SUPR_INFI:
   fixes f :: "nat \<Rightarrow> ereal"
   shows "liminf f = (SUP n. INF m:{n..}. f m)"