src/HOL/Tools/Function/partial_function.ML
changeset 42174 d0be2722ce9f
parent 42083 e1209fc7ecdc
child 42361 23f352990944