src/ZF/Fin.thy
changeset 13244 7b37e218f298
parent 484 70b789956bd3