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