src/HOL/Big_Operators.thy
changeset 53339 0dc28fd72c7d
parent 53174 71a2702da5e0
child 53374 a14d2a854c02