--- a/src/ZF/wf.thy Tue Nov 16 14:23:19 1993 +0100 +++ b/src/ZF/wf.thy Tue Nov 16 14:24:21 1993 +0100 @@ -6,7 +6,7 @@ Well-founded Recursion *) -WF = Trancl + +WF = Trancl + "mono" + consts wf :: "i=>o" wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"