src/HOL/Big_Operators.thy
changeset 36891 e0d295cb8bfd
parent 36635 080b755377c0
child 36977 71c8973a604b