src/ZF/coinductive.thy
changeset 488 52f7447d4f1b
parent 124 858ab9a9b047