changeset 41959 | b460124855b8 |
parent 37765 | 26bdfb7b680b |
child 43704 | 47b0be18ccbe |
41958:5abc60a017e0 | 41959:b460124855b8 |
---|---|
1 (* Title: Archimedean_Field.thy |
1 (* Title: HOL/Archimedean_Field.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 *) |
3 *) |
4 |
4 |
5 header {* Archimedean Fields, Floor and Ceiling Functions *} |
5 header {* Archimedean Fields, Floor and Ceiling Functions *} |
6 |
6 |
7 theory Archimedean_Field |
7 theory Archimedean_Field |