| changeset 35028 | 108662d50512 |
| parent 30102 | 799b687e4aac |
| child 37765 | 26bdfb7b680b |
--- a/src/HOL/Archimedean_Field.thy Fri Feb 05 14:33:31 2010 +0100 +++ b/src/HOL/Archimedean_Field.thy Fri Feb 05 14:33:50 2010 +0100 @@ -12,7 +12,7 @@ text {* Archimedean fields have no infinite elements. *} -class archimedean_field = ordered_field + number_ring + +class archimedean_field = linordered_field + number_ring + assumes ex_le_of_int: "\<exists>z. x \<le> of_int z" lemma ex_less_of_int: