src/HOL/Big_Operators.thy
changeset 54257 5c7a3b6b05a9
parent 54230 b1d955791529
child 54555 e8c5e95d338b