:: deftheorem defines PrimRec COMPUT_1:def 15 :
PrimRec = meet { R where R is Subset of (HFuncs NAT) : R is primitive-recursively_closed } ;