src/HOL/Library/Product_Vector.thy
2015-12-22 immler 2015-12-22 theory for type of bounded linear functions; differentiation under the integral sign
2015-07-06 wenzelm 2015-07-06 tuned proofs;
2015-06-30 paulson 2015-06-30 Useful lemmas. The theorem concerning swapping the variables in a double integral.
2015-06-17 wenzelm 2015-06-17 isabelle update_cartouches;
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-04-11 nipkow 2014-04-11 made divide_pos_pos a simp rule
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-03 hoelzl 2014-04-03 merged DERIV_intros, has_derivative_intros into derivative_intros
2014-04-02 hoelzl 2014-04-02 extend continuous_intros; remove continuous_on_intros and isCont_intros
2014-03-17 hoelzl 2014-03-17 unify syntax for has_derivative and differentiable
2014-01-01 haftmann 2014-01-01 fundamental treatment of undefined vs. universally partial replaces code_abort
2013-12-16 immler 2013-12-16 pragmatic executability of instance prod::{open,dist,norm}
2013-09-26 huffman 2013-09-26 tuned proofs
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
2013-04-09 hoelzl 2013-04-09 add continuous_on rules for products
2013-04-09 hoelzl 2013-04-09 move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
2013-03-22 hoelzl 2013-03-22 move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
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