src/HOL/Big_Operators.thy
changeset 54614 689398f0953f
parent 54555 e8c5e95d338b