src/ZF/Inductive.thy
changeset 74913 c2a2be496f35
parent 74296 abc878973216
child 76213 e44d86131648