src/HOL/Induct/ABexp.ML
changeset 5760 7e2cf2820684
parent 5737 31fc1d0e66d5
child 5802 614f2f30781a