changeset 41959 | b460124855b8 |
parent 37765 | 26bdfb7b680b |
child 43704 | 47b0be18ccbe |
--- a/src/HOL/Archimedean_Field.thy Sun Mar 13 22:24:10 2011 +0100 +++ b/src/HOL/Archimedean_Field.thy Sun Mar 13 22:55:50 2011 +0100 @@ -1,5 +1,5 @@ -(* Title: Archimedean_Field.thy - Author: Brian Huffman +(* Title: HOL/Archimedean_Field.thy + Author: Brian Huffman *) header {* Archimedean Fields, Floor and Ceiling Functions *}