src/HOL/Sum.ML
changeset 1558 9c6ebfab4e05
parent 1515 4ed79ebab64d
child 1760 6f41a494f3b1
equal deleted inserted replaced
1557:fe30812f5b5e 1558:9c6ebfab4e05