src/HOL/Big_Operators.thy
changeset 39598 57413334669d
parent 39302 d7728f65b353
child 40786 0a54cfc9add3
equal deleted inserted replaced
39597:48f63a6c7f85 39598:57413334669d