--- a/Ord.ML Fri Aug 19 11:15:01 1994 +0200
+++ b/Ord.ML Fri Aug 19 11:19:14 1994 +0200
@@ -1,3 +1,11 @@
+(* Title: HOL/Ord.ML
+ ID: $Id$
+ Author: Tobias Nipkow, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+The type class for ordered types
+*)
+
open Ord;
val [prem] = goalw Ord.thy [mono_def]
--- 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