src/ZF/Inductive.thy
changeset 80316 82c20eaad94a
parent 76213 e44d86131648