src/HOL/Induct/Tree.thy
changeset 7990 0a604b2fc2b1
parent 7018 ae18bb3075c3
child 11046 b5f5942781a0