src/HOL/Induct/Tree.thy
changeset 15543 0024472afce7
parent 14981 e73f8140af78
child 16078 e1364521a250