src/HOL/Big_Operators.thy
changeset 52891 b8dede3a4f1d
parent 52379 7f864f2219a9
child 53174 71a2702da5e0