src/ZF/fin.thy
changeset 3967 edd5ff9371f8
parent 124 858ab9a9b047