src/HOL/Induct/Exp.thy
changeset 11481 c77e5401f2ff
parent 5717 0d28dbe484b6