src/HOL/Library/Product_Vector.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
Tue, 04 May 2010 10:42:47 -0700 huffman make (f -- a --> x) an abbreviation for (f ---> x) (at a)
Tue, 04 May 2010 10:06:05 -0700 huffman make (X ----> L) an abbreviation for (X ---> L) sequentially
Sat, 24 Apr 2010 09:37:24 -0700 huffman convert proofs to Isar-style
Sun, 29 Nov 2009 11:31:39 -0800 huffman add lemmas open_image_fst, open_image_snd
Fri, 12 Jun 2009 16:23:07 -0700 huffman declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
Fri, 12 Jun 2009 12:00:30 -0700 huffman remove simp add: norm_scaleR
Thu, 11 Jun 2009 16:26:06 -0700 huffman add lemmas about closed sets
Thu, 11 Jun 2009 11:51:12 -0700 huffman theorem attribute [tendsto_intros]
Thu, 11 Jun 2009 09:03:24 -0700 huffman cleaned up some proofs
Thu, 11 Jun 2009 08:26:08 -0700 huffman new lemmas
Sun, 07 Jun 2009 17:59:54 -0700 huffman replace 'topo' with 'open'; add extra type constraint for 'open'
Sun, 07 Jun 2009 15:18:52 -0700 huffman generalize tendsto lemmas for products
Wed, 03 Jun 2009 09:58:11 -0700 huffman replace class open with class topo
Wed, 03 Jun 2009 08:43:29 -0700 huffman instance * :: topological_space
Tue, 02 Jun 2009 23:35:52 -0700 huffman instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
Mon, 01 Jun 2009 16:59:56 -0700 huffman limits of Pair using filters
Fri, 29 May 2009 09:58:14 -0700 huffman instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
Thu, 28 May 2009 17:09:51 -0700 huffman define dist for products
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Fri, 20 Feb 2009 08:02:11 -0800 huffman add theory of products as real vector spaces to Library
less more (0) tip