src/ZF/ex/primrec0.thy
changeset 4227 a5c947d7c56c
parent 71 729fe026c5f3