src/ZF/fin.thy
changeset 798 31ec33d96231
parent 124 858ab9a9b047