src/ZF/Fin.thy
changeset 6590 fa5f2ca893c5
parent 484 70b789956bd3