src/HOL/Big_Operators.thy
changeset 52879 1df5280f8713
parent 52379 7f864f2219a9
child 53174 71a2702da5e0
equal deleted inserted replaced
52878:8069c8b9335e 52879:1df5280f8713