--- a/src/HOL/Tools/float_syntax.ML Thu Jul 08 16:19:23 2010 +0200
+++ b/src/HOL/Tools/float_syntax.ML Thu Jul 08 16:19:24 2010 +0200
@@ -1,4 +1,5 @@
-(* Author: Tobias Nipkow, TU Muenchen
+(* Title: HOL/Tools/float_syntax.ML
+ Author: Tobias Nipkow, TU Muenchen
Concrete syntax for floats.
*)