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