diff -r 6254f50e5ec9 -r a9f7ff3a464c Ord.thy
--- a/Ord.thy	Fri Sep 16 15:48:20 1994 +0200
+++ b/Ord.thy	Wed Sep 21 15:40:41 1994 +0200
@@ -1,23 +1,25 @@
-(*  Title: 	HOL/Ord.thy
+(*  Title:      HOL/Ord.thy
     ID:         $Id$
-    Author: 	Tobias Nipkow, Cambridge University Computer Laboratory
+    Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-The type class for ordered types
+The type class for ordered types    (* FIXME improve comment *)
 *)
 
 Ord = HOL +
-classes
+
+axclass
   ord < term
+
 consts
   "<", "<="     :: "['a::ord, 'a] => bool"              (infixl 50)
-  mono		:: "['a::ord => 'b::ord] => bool"       (*monotonicity*)
-  min,max	:: "['a::ord,'a] => 'a"
+  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)"
+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
+