src/HOL/MetisExamples/Abstraction.thy
changeset 29923 24f56736c56f
parent 29676 cfa3378decf7
child 31754 b5260f5272a4