src/HOL/Big_Operators.thy
changeset 35995 26e820d27e0a
parent 35938 93faaa15c3d5
child 36079 fa0e354e6a39