src/ZF/Fin.thy
changeset 9927 7a9652294fe0
parent 484 70b789956bd3