1.1 --- a/src/HOL/Lubs.thy	Tue Mar 26 12:20:53 2013 +0100
     1.2 +++ b/src/HOL/Lubs.thy	Tue Mar 26 12:20:54 2013 +0100
     1.3 @@ -94,4 +94,10 @@
     1.4  lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
     1.5    unfolding ubs_def isLub_def by (rule leastPD2)
     1.6  
     1.7 +lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
     1.8 +  apply (frule isLub_isUb)
     1.9 +  apply (frule_tac x = y in isLub_isUb)
    1.10 +  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
    1.11 +  done
    1.12 +
    1.13  end

     2.1 --- a/src/HOL/RComplete.thy	Tue Mar 26 12:20:53 2013 +0100
     2.2 +++ b/src/HOL/RComplete.thy	Tue Mar 26 12:20:54 2013 +0100
     2.3 @@ -8,29 +8,15 @@
     2.4  header {* Completeness of the Reals; Floor and Ceiling Functions *}
     2.5  
     2.6  theory RComplete
     2.7 -imports Conditional_Complete_Lattices RealDef
     2.8 +imports RealDef
     2.9  begin
    2.10  
    2.11 -lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
    2.12 -  by simp
    2.13 -
    2.14 -lemma abs_diff_less_iff:
    2.15 -  "(\<bar>x - a\<bar> < (r::'a::linordered_idom)) = (a - r < x \<and> x < a + r)"
    2.16 -  by auto
    2.17 -
    2.18  subsection {* Completeness of Positive Reals *}
    2.19  
    2.20  text {*
    2.21    \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
    2.22  *}
    2.23  
    2.24 -lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
    2.25 -  apply (frule isLub_isUb)
    2.26 -  apply (frule_tac x = y in isLub_isUb)
    2.27 -  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
    2.28 -  done
    2.29 -
    2.30 -
    2.31  text {*
    2.32    \medskip reals Completeness (again!)
    2.33  *}

     3.1 --- a/src/HOL/RealDef.thy	Tue Mar 26 12:20:53 2013 +0100
     3.2 +++ b/src/HOL/RealDef.thy	Tue Mar 26 12:20:54 2013 +0100
     3.3 @@ -1,7 +1,6 @@
     3.4  (*  Title       : HOL/RealDef.thy
     3.5      Author      : Jacques D. Fleuriot, 1998
     3.6      Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     3.7 -    Additional contributions by Jeremy Avigad
     3.8      Construction of Cauchy Reals by Brian Huffman, 2010
     3.9  *)
    3.10  
    3.11 @@ -1553,6 +1552,8 @@
    3.12  lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"
    3.13    by auto
    3.14  
    3.15 +lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
    3.16 +  by simp
    3.17  
    3.18  subsection{*Absolute Value Function for the Reals*}
    3.19  

     4.1 --- a/src/HOL/Rings.thy	Tue Mar 26 12:20:53 2013 +0100
     4.2 +++ b/src/HOL/Rings.thy	Tue Mar 26 12:20:54 2013 +0100
     4.3 @@ -1143,6 +1143,10 @@
     4.4    "0 \<le> x \<Longrightarrow> \<bar>y\<bar> * x = \<bar>y * x\<bar>"
     4.5    by (simp add: abs_mult)
     4.6  
     4.7 +lemma abs_diff_less_iff:
     4.8 +  "\<bar>x - a\<bar> < r \<longleftrightarrow> a - r < x \<and> x < a + r"
     4.9 +  by (auto simp add: diff_less_eq ac_simps abs_less_iff)
    4.10 +
    4.11  end
    4.12  
    4.13  code_modulename SML