src/HOL/Big_Operators.thy
changeset 51618 a3577cd80c41
parent 51600 197e25f13f0c
child 51738 9e4220605179