src/ZF/Fin.thy
changeset 12725 7ede865e1fe5
parent 484 70b789956bd3