src/ZF/Induct/Binary_Trees.thy
changeset 19597 8ced57ffc090
parent 18415 eb68dc98bda2
child 20503 503ac4c5ef91