src/HOL/Big_Operators.thy
changeset 36348 89c54f51f55a
parent 36303 80e3f43306cf
child 36349 39be26d1bc28