src/HOL/Fun.thy
changeset 20192 956cd30ef3be
parent 20044 92cc2f4c7335
child 21210 c17fd2df4e9e