src/ZF/inductive.thy
changeset 1601 0ef6ea27ab15
parent 124 858ab9a9b047