src/HOL/ex/Summation.thy
changeset 40744 0e7c2957fc1d
parent 39302 d7728f65b353