src/HOL/Multivariate_Analysis/Linear_Algebra.thy
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-22 immler 2015-12-22 theory for type of bounded linear functions; differentiation under the integral sign
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-10-27 paulson 2015-10-27 Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-26 paulson 2015-10-26 new lemmas about topology, etc., for Cauchy integral formula
2015-10-02 paulson 2015-10-02 New theorems about connected sets. And pairwise moved to Set.thy.
2015-09-30 paulson 2015-09-30 real_of_nat_Suc is now a simprule
2015-09-21 wenzelm 2015-09-21 isabelle update_cartouches;
2015-08-19 paulson 2015-08-19 New material and fixes related to the forthcoming Stone-Weierstrass development
2015-07-28 paulson 2015-07-28 tweaks. Got rid of a really slow step
2015-07-27 paulson 2015-07-27 New material for Cauchy's integral theorem
2015-07-20 paulson 2015-07-20 new material for multivariate analysis, etc.
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2015-05-28 paulson 2015-05-28 Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-26 paulson 2015-05-26 New material about paths, and some lemmas
2015-04-30 paulson 2015-04-30 tidying some messy proofs
2015-04-28 paulson 2015-04-28 New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-03-31 paulson 2015-03-31 rationalised and generalised some theorems concerning abs and x^2.
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
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;