src/HOL/Big_Operators.thy
changeset 54574 d04e74341d43
parent 54555 e8c5e95d338b