src/ZF/fin.thy
changeset 5157 6e03de8ec2b4
parent 124 858ab9a9b047