src/HOL/ex/Summation.thy
changeset 42159 234ec7011e5d
parent 39302 d7728f65b353