src/ZF/Induct/Rmap.thy
changeset 80647 3519f026e7d6
parent 76217 8655344f1cf6