src/HOL/Tools/Function/function_common.ML
changeset 39213 297cd703f1f0
parent 39134 917b4b6ba3d2
child 39276 2ad95934521f