src/HOL/Induct/Exp.thy
changeset 9714 79db0e5b7824
parent 5717 0d28dbe484b6