src/HOL/Tools/Function/partial_function.ML
changeset 41648 6d736d983d5c
parent 41472 f6ab14e61604
child 42083 e1209fc7ecdc