--- a/src/HOL/Real.thy Wed Feb 10 08:54:56 2010 +0100
+++ b/src/HOL/Real.thy Wed Feb 10 14:12:02 2010 +0100
@@ -2,25 +2,4 @@
imports RComplete RealVector
begin
-lemma field_le_epsilon:
- fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}"
- assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
- shows "x \<le> y"
-proof (rule ccontr)
- assume xy: "\<not> x \<le> y"
- hence "(x-y)/2 > 0"
- by simp
- hence "x \<le> y + (x - y) / 2"
- by (rule e [of "(x-y)/2"])
- also have "... = (x - y + 2*y)/2"
- by (simp add: diff_divide_distrib)
- also have "... = (x + y) / 2"
- by simp
- also have "... < x" using xy
- by simp
- finally have "x<x" .
- thus False
- by simp
-qed
-
end