src/HOL/Tools/Function/function_lib.ML
changeset 80821 eb383d50564b
parent 74530 823ccd84b879
equal deleted inserted replaced
80820:db114ec720cb 80821:eb383d50564b