diff -r f04b33ce250f -r a4dc62a46ee4 Ord.thy
--- a/Ord.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(*  Title:      HOL/Ord.thy
-    ID:         $Id$
-    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-The type class for ordered types    (* FIXME improve comment *)
-*)
-
-Ord = HOL +
-
-axclass
-  ord < term
-
-consts
-  "<", "<="     :: "['a::ord, 'a] => bool"              (infixl 50)
-  mono          :: "['a::ord => 'b::ord] => bool"       (*monotonicity*)
-  min, max      :: "['a::ord, 'a] => 'a"
-
-defs
-  mono_def      "mono(f)   == (!A B. A <= B --> f(A) <= f(B))"
-  min_def       "min(a, b) == if(a <= b, a, b)"
-  max_def       "max(a, b) == if(a <= b, b, a)"
-
-end
-