src/ZF/fin.thy
changeset 5484 e9430ed7e8d6
parent 124 858ab9a9b047