src/HOL/Big_Operators.thy
changeset 36800 59b50c691b75
parent 36635 080b755377c0
child 36977 71c8973a604b