src/HOL/Big_Operators.thy
changeset 45505 dc452a1a46e5
parent 44937 22c0857b8aab
child 46033 6fc579c917b8
equal deleted inserted replaced
45504:cad35ed6effa 45505:dc452a1a46e5