src/HOL/Tools/Function/partial_function.ML
changeset 77943 ffdad62bc235
parent 77879 dd222e2af01a
child 78072 001739cb8d08