src/ZF/Fin.thy
changeset 13486 54464ea94d6f
parent 484 70b789956bd3