changeset 29988 | 747f0c519090 |
parent 29804 | e15b74577368 |
child 30034 | 60f64f112174 |
--- a/src/HOL/Library/Float.thy Wed Feb 18 20:14:45 2009 -0800 +++ b/src/HOL/Library/Float.thy Wed Feb 18 20:53:58 2009 -0800 @@ -1,7 +1,10 @@ (* Title: HOL/Library/Float.thy * Author: Steven Obua 2008 - * Johannes Hölzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 + * Johannes HÃ\<paragraph>lzl, TU Muenchen <hoelzl@in.tum.de> 2008 / 2009 *) + +header {* Floating-Point Numbers *} + theory Float imports Complex_Main begin