src/HOL/Library/Product_Vector.thy
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