src/HOL/Tools/Function/function_common.ML
changeset 81790 134880dc4df2
parent 81441 29e60ca6ec01
equal deleted inserted replaced
81789:e08eab19cdeb 81790:134880dc4df2