src/ZF/fin.thy
changeset 9303 f1ad1ed0d110
parent 124 858ab9a9b047