src/HOL/Induct/Exp.ML
changeset 3776 38f8ec304b95
parent 3718 d78cf498a88c
child 4089 96fba19bcbe2