src/HOL/Real.thy

--- a/src/HOL/Real.thy	Fri Feb 05 14:33:31 2010 +0100
+++ b/src/HOL/Real.thy	Fri Feb 05 14:33:50 2010 +0100
@@ -3,7 +3,7 @@
 begin
 
 lemma field_le_epsilon:
-  fixes x y :: "'a:: {number_ring,division_by_zero,ordered_field}"
+  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)