src/HOL/Big_Operators.thy
changeset 53792 f0b273258d80
parent 53374 a14d2a854c02
child 54147 97a8ff4e4ac9
equal deleted inserted replaced
53791:0ddf045113c9 53792:f0b273258d80