| Fri, 04 Jul 2014 20:18:47 +0200 | haftmann | reduced name variants for assoc and commute on plus and mult | file | diff | annotate |
| Fri, 01 Nov 2013 18:51:14 +0100 | haftmann | more simplification rules on unary and binary minus | file | diff | annotate |
| Thu, 28 Feb 2013 12:24:24 +0100 | wenzelm | simplified imports; | file | diff | annotate |
| Thu, 31 Jan 2013 17:42:12 +0100 | hoelzl | remove unnecessary assumption from real_normed_vector | file | diff | annotate |
| Mon, 08 Aug 2011 10:32:55 -0700 | huffman | rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too) | file | diff | annotate |
| Thu, 01 Jul 2010 16:54:44 +0200 | haftmann | "prod" and "sum" replace "*" and "+" respectively | file | diff | annotate |
| Thu, 01 Jul 2010 09:01:09 +0200 | hoelzl | Instantiate product type as euclidean space. | file | diff | annotate |
| Sat, 01 May 2010 07:35:22 -0700 | huffman | move setsum lemmas to Product_plus.thy | file | diff | annotate |
| Fri, 20 Feb 2009 07:41:41 -0800 | huffman | add new theory Product_plus.thy to Library | file | diff | annotate |