src/ZF/Induct/Binary_Trees.thy
changeset 18887 6ad81e3fa478
parent 18415 eb68dc98bda2
child 20503 503ac4c5ef91