src/ZF/Fin.thy
changeset 9337 58bd51302b21
parent 484 70b789956bd3