src/HOL/Induct/Exp.thy
changeset 8876 f797816932d7
parent 5717 0d28dbe484b6