src/HOL/ex/Summation.thy
changeset 46368 ded0390eceae
parent 39302 d7728f65b353