diff -r 3716c99fb6a1 -r 5b96b1252cdc Ord.thy
--- a/Ord.thy	Fri Aug 19 11:15:01 1994 +0200
+++ b/Ord.thy	Fri Aug 19 11:19:14 1994 +0200
@@ -1,3 +1,11 @@
+(*  Title: 	HOL/Ord.thy
+    ID:         $Id$
+    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+The type class for ordered types
+*)
+
 Ord = HOL +
 classes
   ord < term