src/HOL/Induct/Exp.thy
changeset 3746 e832a36121ab
parent 3120 c58423c20740
child 4264 5e21f41ccd21