src/HOL/Tools/Function/function.ML
changeset 35403 25a67a606782
parent 35324 c9f428269b38
child 35410 1ea89d2a1bd4
equal deleted inserted replaced
35402:115a5a95710a 35403:25a67a606782