src/HOL/ex/Summation.thy
changeset 49002 8ce0fa01ea86
parent 39302 d7728f65b353
equal deleted inserted replaced
49001:c83370b55e46 49002:8ce0fa01ea86