src/ZF/Induct/Binary_Trees.thy
changeset 14644 3224082514f9
parent 14157 8bf06363bbb5
child 16417 9bc16273c2d4