src/ZF/inductive.thy
changeset 564 eec3a9222b50
parent 124 858ab9a9b047