src/HOL/Induct/ABexp.ML
changeset 8991 dc70b797827f
parent 7847 5a3fa0c4b215