src/HOL/Induct/ABexp.ML
changeset 7018 ae18bb3075c3
parent 5802 614f2f30781a
child 7847 5a3fa0c4b215