src/HOL/Induct/Exp.thy
changeset 12076 8f41684d90e6
parent 5717 0d28dbe484b6