src/HOL/ex/Summation.thy
changeset 50610 d9c4fbbb0c11
parent 39302 d7728f65b353