src/HOL/Big_Operators.thy
2010-03-10 haftmann 2010-03-10 split off theory Big_Operators from theory Finite_Set