src/ZF/Fin.thy
changeset 7991 966efa3bb851
parent 484 70b789956bd3