add header
authorhuffman
Tue Sep 26 22:37:51 2006 +0200 (2006-09-26)
changeset 207172244b0d719a0
parent 20716 a6686a8e1b68
child 20718 4c4869e4ddb7
add header
src/HOL/Real/Float.thy
     1.1 --- a/src/HOL/Real/Float.thy	Tue Sep 26 17:33:04 2006 +0200
     1.2 +++ b/src/HOL/Real/Float.thy	Tue Sep 26 22:37:51 2006 +0200
     1.3 @@ -3,6 +3,8 @@
     1.4      Author: Steven Obua
     1.5  *)
     1.6  
     1.7 +header {* Floating Point Representation of the Reals *}
     1.8 +
     1.9  theory Float
    1.10  imports Real
    1.11  begin