src/ZF/WF.thy

--- a/src/ZF/WF.thy	Tue Mar 07 13:18:48 1995 +0100
+++ b/src/ZF/WF.thy	Tue Mar 07 13:21:38 1995 +0100
@@ -16,7 +16,7 @@
   is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
   the_recfun   :: "[i, i, [i,i]=>i] =>i"
 
-rules
+defs
   (*r is a well-founded relation*)
   wf_def	 "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"