src/HOL/ex/Summation.thy
changeset 48891 c0eafbd55de3
parent 39302 d7728f65b353