src/HOL/Multivariate_Analysis/Linear_Algebra.thy
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-03-22 hoelzl 2013-03-22 introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
2012-11-16 hoelzl 2012-11-16 moved (b)choice_iff(') to Hilbert_Choice
2012-11-16 hoelzl 2012-11-16 move theorems to be more generally useable
2012-10-05 wenzelm 2012-10-05 tuned proofs;
2012-09-29 wenzelm 2012-09-29 tuned proofs;
2012-09-28 wenzelm 2012-09-28 tuned proofs;
2012-09-22 wenzelm 2012-09-22 misc tuning;
2012-09-21 wenzelm 2012-09-21 tuned proofs;
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2011-09-06 huffman 2011-09-06 remove duplicate copy of lemma sqrt_add_le_add_sqrt
2011-09-06 huffman 2011-09-06 remove redundant lemma real_sum_squared_expand in favor of power2_sum
2011-09-02 huffman 2011-09-02 remove more duplicate lemmas
2011-09-01 huffman 2011-09-01 add lemma tendsto_infnorm
2011-08-31 huffman 2011-08-31 remove redundant lemma card_enum
2011-08-25 huffman 2011-08-25 arrange everything related to ordered_euclidean_space class together
2011-08-25 huffman 2011-08-25 generalize and shorten proof of basis_orthogonal
2011-08-25 huffman 2011-08-25 remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}
2011-08-25 huffman 2011-08-25 simplify many proofs about subspace and span; reorder premises in rule span_induct;
2011-08-24 huffman 2011-08-24 minimize imports
2011-08-24 huffman 2011-08-24 move everything related to 'norm' method into new theory file Norm_Arith.thy
2011-08-24 huffman 2011-08-24 remove unused lemmas dimensionI, dimension_eq
2011-08-24 huffman 2011-08-24 move geometric progression lemmas from Linear_Algebra.thy to Integration.thy where they are used
2011-08-23 huffman 2011-08-23 move connected_real_lemma to the one place it is used
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-22 huffman 2011-08-22 avoid warnings
2011-08-22 huffman 2011-08-22 remove duplicate lemma
2011-08-21 huffman 2011-08-21 section -> subsection
2011-08-18 huffman 2011-08-18 import Library/Sum_of_Squares instead of reloading positivstellensatz.ML
2011-08-18 huffman 2011-08-18 declare euclidean_component_zero[simp] at the point it is proved
2011-08-18 huffman 2011-08-18 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
2011-08-12 huffman 2011-08-12 remove redundant lemma setsum_norm in favor of norm_setsum; remove finiteness assumption from setsum_norm_le;
2011-08-12 huffman 2011-08-12 make Multivariate_Analysis work with separate set type
2011-08-11 huffman 2011-08-11 modify euclidean_space class to include basis set
2011-08-10 huffman 2011-08-10 avoid warnings about duplicate rules
2011-08-10 huffman 2011-08-10 split Linear_Algebra.thy from Euclidean_Space.thy