src/HOL/Big_Operators.thy
changeset 46544 460b0d81d486
parent 46033 6fc579c917b8
child 46554 87d4e4958476