src/ZF/inductive.thy
changeset 7924 5fee69b1f5fe
parent 124 858ab9a9b047