src/ZF/Induct/Rmap.thy
changeset 78534 879e1ba3868b
parent 76217 8655344f1cf6