# HG changeset patch
# User huffman
# Date 1159303071 -7200
# Node ID 2244b0d719a06e976482a1c7538aea2cbe294f42
# Parent  a6686a8e1b687a5cb2ebb6774114cb35df3a14ee
add header

diff -r a6686a8e1b68 -r 2244b0d719a0 src/HOL/Real/Float.thy
--- 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