src/HOL/Fun.ML
changeset 10819 4e056473ae30
parent 10076 2683ff181047
child 10826 f3b7201dda27