src/ZF/Fin.thy
changeset 11612 ae8450657bf0
parent 484 70b789956bd3