equal
deleted
inserted
replaced
10 |
10 |
11 subsection {* Class of Archimedean fields *} |
11 subsection {* Class of Archimedean fields *} |
12 |
12 |
13 text {* Archimedean fields have no infinite elements. *} |
13 text {* Archimedean fields have no infinite elements. *} |
14 |
14 |
15 class archimedean_field = ordered_field + number_ring + |
15 class archimedean_field = linordered_field + number_ring + |
16 assumes ex_le_of_int: "\<exists>z. x \<le> of_int z" |
16 assumes ex_le_of_int: "\<exists>z. x \<le> of_int z" |
17 |
17 |
18 lemma ex_less_of_int: |
18 lemma ex_less_of_int: |
19 fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z" |
19 fixes x :: "'a::archimedean_field" shows "\<exists>z. x < of_int z" |
20 proof - |
20 proof - |