src/ZF/Inductive.thy
changeset 69980 f2e3adfd916f
parent 69605 a96320074298
child 74296 abc878973216