src/HOL/Library/Product_plus.thy
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-02-28 wenzelm 2013-02-28 simplified imports;
2013-01-31 hoelzl 2013-01-31 remove unnecessary assumption from real_normed_vector
2011-08-08 huffman 2011-08-08 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-07-01 hoelzl 2010-07-01 Instantiate product type as euclidean space.
2010-05-01 huffman 2010-05-01 move setsum lemmas to Product_plus.thy
2009-02-20 huffman 2009-02-20 add new theory Product_plus.thy to Library