src/HOL/Library/Product_Vector.thy
2013-01-31 hoelzl 2013-01-31 remove unnecessary assumption from real_normed_vector
2012-10-19 webertj 2012-10-19 Renamed {left,right}_distrib to distrib_{right,left}.
2011-09-06 huffman 2011-09-06 remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-08-29 huffman 2011-08-29 Product_Vector.thy: clean up some proofs
2011-08-28 huffman 2011-08-28 discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-16 huffman 2011-08-16 add simp rules for isCont
2011-08-15 huffman 2011-08-15 Library/Product_Vector.thy: class instances for t0_space, t1_space, and t2_space
2011-08-09 huffman 2011-08-09 lemma bounded_linear_intro
2011-08-09 huffman 2011-08-09 avoid duplicate rewrite warnings
2011-08-08 huffman 2011-08-08 rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-05-04 huffman 2010-05-04 make (f -- a --> x) an abbreviation for (f ---> x) (at a)
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