diff -r 3716c99fb6a1 -r 5b96b1252cdc Ord.ML --- 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]