src/HOL/Induct/ABexp.ML
changeset 7596 c97c3ad15d2e
parent 5802 614f2f30781a
child 7847 5a3fa0c4b215
equal deleted inserted replaced
7595:5f5d575ddac3 7596:c97c3ad15d2e