src/ZF/Fin.thy
changeset 2944 283e31f6a4be
parent 484 70b789956bd3