src/ZF/Fin.thy
changeset 9577 9e66e8ed8237
parent 484 70b789956bd3