| changeset 30122 | 1c912a9d8200 |
| parent 30034 | 60f64f112174 |
| child 30181 | 05629f28f0f7 |
--- a/src/HOL/Library/Float.thy Thu Feb 26 20:55:47 2009 +0100 +++ b/src/HOL/Library/Float.thy Thu Feb 26 20:56:59 2009 +0100 @@ -1,7 +1,7 @@ -(* Title: HOL/Library/Float.thy - * Author: Steven Obua 2008 - * Johannes HÃ\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 - *) +(* Title: HOL/Library/Float.thy + Author: Steven Obua 2008 + Author: Johannes Hoelzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 +*) header {* Floating-Point Numbers *}