src/HOL/MetisExamples/Abstraction.thy
changeset 30819 17bd1cf53d8e
parent 29676 cfa3378decf7
child 31754 b5260f5272a4