src/HOL/Tools/Function/function.ML
changeset 35624 c4e29a0bb8c1
parent 35410 1ea89d2a1bd4
child 35756 cfde251d03a5