src/ZF/coinductive.thy
changeset 3522 a34c20f4bf44
parent 124 858ab9a9b047