src/HOL/Tools/Function/partial_function.ML
changeset 60987 ea00d17eba3b
parent 60784 4f590c08fd5d
child 61113 86049d52155c