src/HOL/MetisExamples/Abstraction.thy
changeset 29813 3ccd86c214bf
parent 29676 cfa3378decf7
child 31754 b5260f5272a4