src/HOL/MetisExamples/Abstraction.thy
changeset 29270 0eade173f77e
parent 28592 824f8390aaa2
child 29676 cfa3378decf7