src/HOL/Big_Operators.thy
changeset 52861 e93d73b51fd0
parent 52379 7f864f2219a9
child 53174 71a2702da5e0
equal deleted inserted replaced
52860:f155c38242c1 52861:e93d73b51fd0