--- a/src/HOL/Real/Float.thy Tue Sep 26 17:33:04 2006 +0200 +++ b/src/HOL/Real/Float.thy Tue Sep 26 22:37:51 2006 +0200 @@ -3,6 +3,8 @@ Author: Steven Obua *) +header {* Floating Point Representation of the Reals *} + theory Float imports Real begin