src/ZF/Inductive.thy
changeset 81305 e85b5f7f9b16
parent 76213 e44d86131648