--- a/src/HOL/RComplete.thy Tue Mar 26 12:20:53 2013 +0100
+++ b/src/HOL/RComplete.thy Tue Mar 26 12:20:54 2013 +0100
@@ -8,29 +8,15 @@
header {* Completeness of the Reals; Floor and Ceiling Functions *}
theory RComplete
-imports Conditional_Complete_Lattices RealDef
+imports RealDef
begin
-lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
- by simp
-
-lemma abs_diff_less_iff:
- "(\<bar>x - a\<bar> < (r::'a::linordered_idom)) = (a - r < x \<and> x < a + r)"
- by auto
-
subsection {* Completeness of Positive Reals *}
text {*
\medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
*}
-lemma real_isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::real)"
- apply (frule isLub_isUb)
- apply (frule_tac x = y in isLub_isUb)
- apply (blast intro!: order_antisym dest!: isLub_le_isUb)
- done
-
-
text {*
\medskip reals Completeness (again!)
*}