src/HOL/Induct/ABexp.ML
changeset 7825 1be9b63e7d93
parent 5802 614f2f30781a
child 7847 5a3fa0c4b215