src/HOL/ex/Functions.thy
changeset 73255 7e2a9a8c2b85
parent 70468 8406a2c296e0