src/HOL/Multivariate_Analysis/Linear_Algebra.thy
2014-03-16 haftmann 2014-03-16 normalising simp rules for compound operators
2014-03-04 huffman 2014-03-04 tuned proof
2014-02-27 paulson 2014-02-27 A bit of tidying up
2014-01-25 wenzelm 2014-01-25 tuned proof;
2013-12-16 immler 2013-12-16 summarized notions related to ordered_euclidean_space and intervals in separate theory
2013-12-16 immler 2013-12-16 introduced ordered real vector spaces
2013-12-16 immler 2013-12-16 ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-12 hoelzl 2013-11-12 add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-09-26 huffman 2013-09-26 tuned proofs
2013-09-26 huffman 2013-09-26 moved lemma
2013-09-24 wenzelm 2013-09-24 tuned proofs;
2013-09-18 wenzelm 2013-09-18 tuned proofs;
2013-09-12 huffman 2013-09-12 make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
2013-09-12 huffman 2013-09-12 new lemmas
2013-09-12 huffman 2013-09-12 prefer theorem name over 'long_thm_list(n)'
2013-09-04 wenzelm 2013-09-04 tuned proofs;
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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