src/HOL/Induct/Tree.thy
changeset 9750 270cd9831e7b
parent 7018 ae18bb3075c3
child 11046 b5f5942781a0