src/HOL/Multivariate_Analysis/Linear_Algebra.thy
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann 2014-06-28 fact consolidation
2014-04-11 nipkow 2014-04-11 made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl 2014-04-09 field_simps: better support for negation and division, and power
2014-04-09 hoelzl 2014-04-09 revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-06 wenzelm 2014-04-06 tuned proofs;
2014-04-03 paulson 2014-04-03 removing simprule status for divide_minus_left and divide_minus_right
2014-03-18 huffman 2014-03-18 remove unnecessary finiteness assumptions from lemmas about setsum
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