src/HOL/Library/Product_Vector.thy
2010-05-04 huffman 2010-05-04 make (X ----> L) an abbreviation for (X ---> L) sequentially
2010-04-24 huffman 2010-04-24 convert proofs to Isar-style
2009-11-29 huffman 2009-11-29 add lemmas open_image_fst, open_image_snd
2009-06-12 huffman 2009-06-12 declare inner_add, inner_diff [algebra_simps]; declare inner_scaleR [simp]
2009-06-12 huffman 2009-06-12 remove simp add: norm_scaleR
2009-06-11 huffman 2009-06-11 add lemmas about closed sets
2009-06-11 huffman 2009-06-11 theorem attribute [tendsto_intros]
2009-06-11 huffman 2009-06-11 cleaned up some proofs
2009-06-11 huffman 2009-06-11 new lemmas
2009-06-07 huffman 2009-06-07 replace 'topo' with 'open'; add extra type constraint for 'open'
2009-06-07 huffman 2009-06-07 generalize tendsto lemmas for products
2009-06-03 huffman 2009-06-03 replace class open with class topo
2009-06-03 huffman 2009-06-03 instance * :: topological_space
2009-06-02 huffman 2009-06-02 instance * :: complete_space; generalize continuity lemmas for fst, snd, Pair
2009-06-01 huffman 2009-06-01 limits of Pair using filters
2009-05-29 huffman 2009-05-29 instance * :: (metric_space, metric_space) metric_space; generalize lemmas to class metric_space
2009-05-28 huffman 2009-05-28 define dist for products
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-02-20 huffman 2009-02-20 add theory of products as real vector spaces to Library