src/HOL/Fun.ML
changeset 11979 0a3dace545c5
parent 11601 9273cef990f5
child 12338 de0f4a63baa5