src/HOL/Real/Real.thy

--- a/src/HOL/Real/Real.thy	Fri Jul 23 17:28:18 1999 +0200
+++ b/src/HOL/Real/Real.thy	Fri Jul 23 17:29:12 1999 +0200
@@ -1,9 +1,8 @@
-(*  Title:      Real/Real.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Type "real" is a linear order
+(*  Title:       Real/Real.thy
+    Author:      Lawrence C. Paulson
+                 Jacques D. Fleuriot
+    Copyright:   1998  University of Cambridge
+    Description: Type "real" is a linear order
 *)
 
 Real = RealDef +