src/HOL/Tools/Function/partial_function.ML
changeset 42966 4e2d6c1e5392
parent 42949 618adb3584e5
child 43080 73a1d6a7ef1d