src/ZF/Fin.thy
changeset 9220 d0506ced27c8
parent 484 70b789956bd3