src/ZF/Inductive_ZF.thy
changeset 28919 88b8cc1a2983
parent 26480 544cef16045b
child 29580 117b88da143c