diff -r 059c3568fdc8 -r abc6a2ea4b88 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Fri Apr 02 13:33:48 2010 +0200
+++ b/src/HOL/Real.thy	Wed Apr 07 19:17:10 2010 +0200
@@ -2,28 +2,4 @@
 imports RComplete RealVector
 begin
 
-lemma field_le_epsilon:
-  fixes x y :: "'a:: {number_ring,division_by_zero,ordered_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 (metis half_gt_zero le_iff_diff_le_0 linorder_not_le local.xy)
-  hence "x \<le> y + (x - y) / 2"
-    by (rule e [of "(x-y)/2"])
-  also have "... = (x - y + 2*y)/2"
-    by auto
-       (metis add_less_cancel_left add_numeral_0_right class_semiring.add_c xy e
-           diff_add_cancel gt_half_sum less_half_sum linorder_not_le number_of_Pls)
-  also have "... = (x + y) / 2" 
-    by auto
-  also have "... < x" using xy 
-    by auto
-  finally have "x<x" .
-  thus False
-    by auto 
-qed
-
-
 end