src/HOL/WF.thy
changeset 972 e61b058d58d2
parent 965 24eef3860714
child 1276 42ccfd3e1fb4
     1.1 --- a/src/HOL/WF.thy	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/WF.thy	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -15,9 +15,9 @@
     1.4     the_recfun	:: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b"
     1.5  
     1.6  defs
     1.7 -  wf_def  "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
     1.8 +  wf_def  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
     1.9    
    1.10 -  cut_def 	 "cut f r x == (%y. if <y,x>:r then f y else @z.True)"
    1.11 +  cut_def 	 "cut f r x == (%y. if (y,x):r then f y else @z.True)"
    1.12  
    1.13    is_recfun_def  "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
    1.14