src/ZF/Induct/Rmap.thy
changeset 80108 6ec65767d7bd
parent 76217 8655344f1cf6