# HG changeset patch
# User oheimb
# Date 982249242 -3600
# Node ID 9265b6415d76ffc9f9d5173b88004bf4f16193e5
# Parent  e34e7f6d9b571e2c903d8e012c8044da368970cb
added wellorder axclass

diff -r e34e7f6d9b57 -r 9265b6415d76 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