src/HOL/Big_Operators.thy
changeset 39655 8ad7fe9d6f0b
parent 39302 d7728f65b353
child 40786 0a54cfc9add3
equal deleted inserted replaced
39654:1207e39f0c7f 39655:8ad7fe9d6f0b