src/ZF/Induct/Binary_Trees.thy
changeset 81156 cf750881f1fe
parent 76217 8655344f1cf6