1.1 --- a/NEWS	Fri Sep 02 15:19:59 2011 -0700
     1.2 +++ b/NEWS	Fri Sep 02 16:48:30 2011 -0700
     1.3 @@ -274,6 +274,7 @@
     1.4    realpow_two_disj ~> power2_eq_iff
     1.5    real_squared_diff_one_factored ~> square_diff_one_factored
     1.6    realpow_two_diff ~> square_diff_square_factored
     1.7 +  reals_complete2 ~> complete_real
     1.8    exp_ln_eq ~> ln_unique
     1.9    lemma_DERIV_subst ~> DERIV_cong
    1.10    LIMSEQ_Zfun_iff ~> tendsto_Zfun_iff

     2.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Sep 02 15:19:59 2011 -0700
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Sep 02 16:48:30 2011 -0700
     2.3 @@ -1110,7 +1110,7 @@
     2.4      with `S \<noteq> {}` `\<infinity> \<notin> S` obtain x where "x \<in> S - {-\<infinity>}" "x \<noteq> \<infinity>" by auto
     2.5      with y `\<infinity> \<notin> S` have "\<forall>z\<in>real ` (S - {-\<infinity>}). z \<le> y"
     2.6        by (auto simp: real_of_ereal_ord_simps)
     2.7 -    with reals_complete2[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
     2.8 +    with complete_real[of "real ` (S - {-\<infinity>})"] `x \<in> S - {-\<infinity>}`
     2.9      obtain s where s:
    2.10         "\<forall>y\<in>S - {-\<infinity>}. real y \<le> s" "\<And>z. (\<forall>y\<in>S - {-\<infinity>}. real y \<le> z) \<Longrightarrow> s \<le> z"
    2.11         by auto

     3.1 --- a/src/HOL/RComplete.thy	Fri Sep 02 15:19:59 2011 -0700
     3.2 +++ b/src/HOL/RComplete.thy	Fri Sep 02 16:48:30 2011 -0700
     3.3 @@ -80,14 +80,6 @@
     3.4        Collect_def mem_def isUb_def UNIV_def by simp
     3.5  qed
     3.6  
     3.7 -text{*A version of the same theorem without all those predicates!*}
     3.8 -lemma reals_complete2:
     3.9 -  fixes S :: "(real set)"
    3.10 -  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
    3.11 -  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
    3.12 -               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
    3.13 -using assms by (rule complete_real)
    3.14 -
    3.15  
    3.16  subsection {* The Archimedean Property of the Reals *}
    3.17  

     4.1 --- a/src/HOL/SupInf.thy	Fri Sep 02 15:19:59 2011 -0700
     4.2 +++ b/src/HOL/SupInf.thy	Fri Sep 02 16:48:30 2011 -0700
     4.3 @@ -30,7 +30,7 @@
     4.4        and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
     4.5    shows "x \<le> Sup X"
     4.6  proof (auto simp add: Sup_real_def) 
     4.7 -  from reals_complete2
     4.8 +  from complete_real
     4.9    obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
    4.10      by (blast intro: x z)
    4.11    hence "x \<le> s"
    4.12 @@ -46,7 +46,7 @@
    4.13        and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    4.14    shows "Sup X \<le> z"
    4.15  proof (auto simp add: Sup_real_def) 
    4.16 -  from reals_complete2 x
    4.17 +  from complete_real x
    4.18    obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
    4.19      by (blast intro: z)
    4.20    hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
    4.21 @@ -119,7 +119,7 @@
    4.22      apply (metis ex_in_conv x)
    4.23      apply (rule Sup_upper_EX) 
    4.24      apply blast
    4.25 -    apply (metis insert_iff linear order_refl order_trans z)
    4.26 +    apply (metis insert_iff linear order_trans z)
    4.27      done
    4.28    moreover 
    4.29    have "Sup (insert a X) \<le> Sup X"
    4.30 @@ -333,7 +333,7 @@
    4.31      apply (metis ex_in_conv x)
    4.32      apply (rule Inf_lower_EX)
    4.33      apply (erule insertI2)
    4.34 -    apply (metis insert_iff linear order_refl order_trans z)
    4.35 +    apply (metis insert_iff linear order_trans z)
    4.36      done
    4.37    moreover 
    4.38    have "Inf X \<le> Inf (insert a X)"