src/HOL/MetisExamples/Abstraction.thy
changeset 26964 df1f238a05f7
parent 26819 56036226028b
child 27368 9f90ac19e32b