src/HOL/Induct/Exp.ML
changeset 3712 242546f35f8e
parent 3145 809a2c9902f7
child 3718 d78cf498a88c