src/ZF/Induct/Binary_Trees.thy
changeset 82369 eae75676ecd7
parent 76217 8655344f1cf6