changeset 35028 | 108662d50512 |
parent 32877 | 6f09346c7c08 |
child 35066 | 894e82be8d05 |
--- 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)