src/ZF/WF.thy
changeset 1401 0c439768f45c
parent 1155 928a16e02f9f
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/WF.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/WF.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,13 +8,13 @@
     1.4  
     1.5  WF = Trancl + "mono" + "equalities" +
     1.6  consts
     1.7 -  wf           :: "i=>o"
     1.8 -  wf_on        :: "[i,i]=>o"			("wf[_]'(_')")
     1.9 +  wf           :: i=>o
    1.10 +  wf_on        :: [i,i]=>o			("wf[_]'(_')")
    1.11  
    1.12 -  wftrec,wfrec :: "[i, i, [i,i]=>i] =>i"
    1.13 -  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"	("wfrec[_]'(_,_,_')")
    1.14 -  is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
    1.15 -  the_recfun   :: "[i, i, [i,i]=>i] =>i"
    1.16 +  wftrec,wfrec :: [i, i, [i,i]=>i] =>i
    1.17 +  wfrec_on     :: [i, i, i, [i,i]=>i] =>i	("wfrec[_]'(_,_,_')")
    1.18 +  is_recfun    :: [i, i, [i,i]=>i, i] =>o
    1.19 +  the_recfun   :: [i, i, [i,i]=>i] =>i
    1.20  
    1.21  defs
    1.22    (*r is a well-founded relation*)