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