src/HOL/Big_Operators.thy
changeset 49918 cf441f4a358b
parent 49715 16d8c6d288bc
child 49962 a8cc904a6820