src/HOL/Big_Operators.thy
changeset 41101 c1d1ec5b90f1
parent 40786 0a54cfc9add3
child 41550 efa734d9b221
equal deleted inserted replaced
41100:6c0940392fb4 41101:c1d1ec5b90f1