src/HOL/Wellfounded_Recursion.thy

--- a/src/HOL/Wellfounded_Recursion.thy	Thu Feb 15 16:00:40 2001 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Thu Feb 15 16:00:42 2001 +0100
@@ -28,4 +28,8 @@
   "wfrec r H == (%x. H (cut (the_recfun (trancl r) (%f v. H (cut f r v) v) x)
                             r x)  x)"
 
+axclass
+  wellorder < linorder
+  wf "wf {(x,y::'a::ord). x<y}"
+
 end