src/HOL/WF.thy
changeset 965 24eef3860714
parent 923 ff1574a81019
child 972 e61b058d58d2
     1.1 --- a/src/HOL/WF.thy	Fri Mar 17 22:46:26 1995 +0100
     1.2 +++ b/src/HOL/WF.thy	Mon Mar 20 15:35:28 1995 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  defs
     1.5    wf_def  "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))"
     1.6    
     1.7 -  cut_def 	 "cut f r x == (%y. if (<y,x>:r) (f y) (@z.True))"
     1.8 +  cut_def 	 "cut f r x == (%y. if <y,x>:r then f y else @z.True)"
     1.9  
    1.10    is_recfun_def  "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)"
    1.11