src/HOL/Induct/Exp.thy
changeset 5089 f95e0a6eb775
parent 4264 5e21f41ccd21
child 5717 0d28dbe484b6