src/ZF/Induct/Binary_Trees.thy
changeset 14427 cea7d2f76112
parent 14157 8bf06363bbb5
child 16417 9bc16273c2d4