src/ZF/coinductive.thy
changeset 4223 f60e3d2c81d3
parent 124 858ab9a9b047