src/HOL/Library/Product_plus.thy
Mon, 08 Aug 2011 10:32:55 -0700 huffman rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
Thu, 01 Jul 2010 16:54:44 +0200 haftmann "prod" and "sum" replace "*" and "+" respectively
Thu, 01 Jul 2010 09:01:09 +0200 hoelzl Instantiate product type as euclidean space.
Sat, 01 May 2010 07:35:22 -0700 huffman move setsum lemmas to Product_plus.thy
Fri, 20 Feb 2009 07:41:41 -0800 huffman add new theory Product_plus.thy to Library
less more (0) tip