src/HOL/Induct/Tree.thy
changeset 9789 7e5e6c47c0b5
parent 7018 ae18bb3075c3
child 11046 b5f5942781a0