added wellorder axclass
authoroheimb
Thu, 15 Feb 2001 16:00:42 +0100
changeset 11137 9265b6415d76
parent 11136 e34e7f6d9b57
child 11138 bdfb9ec76a0a
added wellorder axclass
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