src/HOL/Fun.ML
changeset 4081 f759352f669f
parent 4059 59c1422c9da5
child 4089 96fba19bcbe2