src/ZF/Induct/Binary_Trees.thy
changeset 69587 53982d5ec0bb
parent 67443 3abf6a722518
child 69593 3dda49e08b9d