src/HOL/Big_Operators.thy
changeset 54492 6fae4ecd4ab3
parent 54230 b1d955791529
child 54555 e8c5e95d338b