src/ZF/inductive.thy
changeset 9230 17ae63f82ad8
parent 124 858ab9a9b047