src/HOL/Tools/Function/partial_function.ML
changeset 41836 c9d788ff7940
parent 41472 f6ab14e61604
child 42083 e1209fc7ecdc
equal deleted inserted replaced
41835:9712fae15200 41836:c9d788ff7940