src/ZF/Induct/Primrec.thy
changeset 18924 83acd39b1bab
parent 18415 eb68dc98bda2
child 19676 187234ec6050