src/HOL/Tools/Function/partial_function.ML
changeset 61011 018b0c996b54
parent 60784 4f590c08fd5d
child 61113 86049d52155c