src/HOL/Tools/function_package/pattern_split.ML
changeset 26088 9b48d0264ffd
parent 25538 58e8ba3b792b
child 27330 1af2598b5f7d
equal deleted inserted replaced
26087:454a5456a4b5 26088:9b48d0264ffd