src/ZF/Inductive.thy
changeset 82902 99a720d3ed8f
parent 76213 e44d86131648