src/HOL/Fun.thy
changeset 17943 48ec47217fe2
parent 17877 67d5ab1cb0d8
child 17956 369e2af8ee45