1.1 --- a/src/HOL/Library/Extended_Real.thy	Thu Jul 21 21:56:24 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 21 22:47:13 2011 +0200
     1.3 @@ -1338,33 +1338,6 @@
     1.4      by (cases e) auto
     1.5  qed
     1.6  
     1.7 -lemma (in complete_linorder) Sup_eq_top_iff: -- "FIXME move"
     1.8 -  "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
     1.9 -proof
    1.10 -  assume *: "Sup A = top"
    1.11 -  show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
    1.12 -  proof (intro allI impI)
    1.13 -    fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
    1.14 -      unfolding less_Sup_iff by auto
    1.15 -  qed
    1.16 -next
    1.17 -  assume *: "\<forall>x<top. \<exists>i\<in>A. x < i"
    1.18 -  show "Sup A = top"
    1.19 -  proof (rule ccontr)
    1.20 -    assume "Sup A \<noteq> top"
    1.21 -    with top_greatest [of "Sup A"]
    1.22 -    have "Sup A < top" unfolding le_less by auto
    1.23 -    then have "Sup A < Sup A"
    1.24 -      using * unfolding less_Sup_iff by auto
    1.25 -    then show False by auto
    1.26 -  qed
    1.27 -qed
    1.28 -
    1.29 -lemma (in complete_linorder) SUP_eq_top_iff: -- "FIXME move"
    1.30 -  fixes f :: "'b \<Rightarrow> 'a"
    1.31 -  shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
    1.32 -  unfolding SUPR_def Sup_eq_top_iff by auto
    1.33 -
    1.34  lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
    1.35  proof -
    1.36    { fix x ::ereal assume "x \<noteq> \<infinity>"
    1.37 @@ -2374,14 +2347,6 @@
    1.38  
    1.39  abbreviation "limsup \<equiv> Limsup sequentially"
    1.40  
    1.41 -lemma (in complete_lattice) less_INFD:
    1.42 -  assumes "y < INFI A f"" i \<in> A" shows "y < f i"
    1.43 -proof -
    1.44 -  note `y < INFI A f`
    1.45 -  also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI)
    1.46 -  finally show "y < f i" .
    1.47 -qed
    1.48 -
    1.49  lemma liminf_SUPR_INFI:
    1.50    fixes f :: "nat \<Rightarrow> ereal"
    1.51    shows "liminf f = (SUP n. INF m:{n..}. f m)"