src/ZF/coinductive.thy
changeset 7145 c05373eebee3
parent 124 858ab9a9b047