src/HOL/Big_Operators.thy
changeset 36822 38a480e0346f
parent 36635 080b755377c0
child 36977 71c8973a604b
equal deleted inserted replaced
36821:9207505d1ee5 36822:38a480e0346f