src/ZF/Fin.thy
changeset 854 2e3ca37dfa14
parent 484 70b789956bd3