src/ZF/Fin.thy
changeset 3511 da4dd8b7ced4
parent 484 70b789956bd3