src/ZF/Fin.thy
changeset 5137 60205b0de9b9
parent 484 70b789956bd3