src/ZF/Fin.thy
changeset 7566 c5a3f980a7af
parent 484 70b789956bd3