src/HOL/Library/Rational_Numbers.thy

--- a/src/HOL/Library/Rational_Numbers.thy	Fri Dec 15 17:59:30 2000 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy	Fri Dec 15 17:59:45 2000 +0100
@@ -1,3 +1,8 @@
+(*  Title:      HOL/Library/Rational_Numbers.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+*)
 
 header {*
   \title{Rational numbers}