src/HOL/Tools/Function/partial_function.ML
changeset 60107 aedbc0413d30
parent 59936 b8ffc3dc9e24
child 60642 48dd1cefb4ae
equal deleted inserted replaced
60106:e0d1d9203275 60107:aedbc0413d30