--- a/WF.thy	Thu Nov 24 20:11:40 1994 +0100
+++ b/WF.thy	Thu Nov 24 20:31:09 1994 +0100
@@ -14,7 +14,7 @@
    is_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b, 'a=>'b] => bool"
    the_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
 
-rules
+defs
   wf_def  "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
   
   cut_def 	 "cut(f,r,x) == (%y. if(<y,x>:r, f(y), @z.True))"