src/HOL/Induct/Exp.thy
changeset 12873 d7f8dfaad46d
parent 5717 0d28dbe484b6