src/HOL/ex/Summation.thy
changeset 49002 8ce0fa01ea86
parent 39302 d7728f65b353