src/HOL/Library/Product_plus.thy
2009-02-20 huffman 2009-02-20 add new theory Product_plus.thy to Library