src/HOL/Tools/Function/function_common.ML
changeset 39213 297cd703f1f0
parent 39134 917b4b6ba3d2
child 39276 2ad95934521f
equal deleted inserted replaced
39212:3989b2b44dba 39213:297cd703f1f0