src/ZF/Induct/Comb.thy
changeset 14024 213dcc39358f
parent 13573 37b22343c35a
child 15775 d8dd2fffa692