changeset 178 | 12dd5d2e266b |
parent 0 | 7949f97df77a |
--- 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))"