src/HOL/Big_Operators.thy
changeset 51667 354c23ef2784
parent 51600 197e25f13f0c
child 51738 9e4220605179
equal deleted inserted replaced
51652:5ff01d585a8c 51667:354c23ef2784