src/HOL/Tools/Function/partial_function.ML
changeset 42224 578a51fae383
parent 42083 e1209fc7ecdc
child 42361 23f352990944