src/ZF/Induct/Binary_Trees.thy
changeset 24067 69b51bc5ce06
parent 20503 503ac4c5ef91
child 24893 b8ef7afe3a6b