src/ZF/inductive.thy
changeset 12902 a23dc0b7566f
parent 124 858ab9a9b047