src/HOL/Sum.ML
changeset 1558 9c6ebfab4e05
parent 1515 4ed79ebab64d
child 1760 6f41a494f3b1