src/HOL/Tools/Function/function.ML
changeset 44232 d5f689c534c5
parent 44192 a32ca9165928
child 44239 47ecd30e018d