src/ZF/Constructible/Rec_Separation.thy
2002-07-12 paulson 2002-07-12 new definitions of fun_apply and M_is_recfun
2002-07-11 paulson 2002-07-11 Separation/Replacement up to M_wfrank!