src/ZF/inductive.thy
changeset 8913 0bc13d5e60b8
parent 124 858ab9a9b047