src/HOL/Library/Product_Plus.thy
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-30 hoelzl 2016-09-30 Library: fix name Product_plus to Product_Plus