src/HOL/Tools/Function/function_common.ML
changeset 50895 3a1edaa0dc6d
parent 49979 4de92b4aa74a
child 52383 71df93ff010d
equal deleted inserted replaced
50894:a9c1b1428e87 50895:3a1edaa0dc6d