src/HOL/Tools/function_package/sum_tools.ML
changeset 23315 df3a7e9ebadb
parent 22622 25693088396b
equal deleted inserted replaced
23314:6894137e854a 23315:df3a7e9ebadb