src/ZF/Induct/Binary_Trees.thy
changeset 14024 213dcc39358f
parent 12194 13909cb72129
child 14157 8bf06363bbb5