src/ZF/Inductive.thy
changeset 81697 1629c2ff4880
parent 76213 e44d86131648