author | huffman |
Wed, 18 Feb 2009 20:53:58 -0800 | |
changeset 29988 | 747f0c519090 |
parent 29987 | 391dcbd7e4dd |
child 29989 | bdf83fc2c8ba |
--- 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