src/HOL/Induct/Tree.thy
changeset 43657 537ea3846f64
parent 39246 9e58f0499f57
child 46914 c2ca2c3d23a6