src/HOL/Induct/Exp.thy
changeset 8383 2dd4823c744f
parent 5717 0d28dbe484b6