--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Ord.thy	Thu Sep 16 12:21:07 1993 +0200
@@ -0,0 +1,15 @@
+Ord = HOL +
+classes
+  ord < term
+consts
+  "<", "<="     :: "['a::ord, 'a] => bool"              (infixl 50)
+  mono		:: "['a::ord => 'b::ord] => bool"       (*monotonicity*)
+  min,max	:: "['a::ord,'a] => 'a"
+
+rules
+
+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