src/ZF/Inductive.thy
changeset 83240 dfa14d921fd2
parent 76213 e44d86131648