src/HOL/Multivariate_Analysis/Linear_Algebra.thy
2016-05-23 paulson Lots of new material for multivariate analysis
2016-05-09 paulson lemmas about dimension, hyperplanes, span, etc.
2016-05-09 paulson renamings and refinements
2016-04-22 hoelzl Linear_Algebra: generalize linear_surjective_right/injective_left_inverse to real vector spaces
2016-04-22 hoelzl Linear_Algebra: generalize linear_independent_extend to all real vector spaces
2016-04-22 hoelzl Linear_Algebra: alternative representation of linear combination
2016-04-22 hoelzl Linear_Algebra: move abstract concepts to front
2016-04-18 paulson new theorems about convex hulls, etc.; also, renamed some theorems
2016-04-11 paulson lots of new theorems for multivariate analysis
2016-03-15 paulson rationalisation of theorem names esp about "real Archimedian" etc.
2016-02-24 paulson Substantial new material for multivariate analysis. Also removal of some duplicates.
2016-02-17 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
2015-12-30 wenzelm more symbols;
2015-12-22 immler theory for type of bounded linear functions; differentiation under the integral sign
2015-12-07 wenzelm isabelle update_cartouches -c -t;
2015-11-10 paulson 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 Cauchy's integral formula, required lemmas, and a bit of reorganisation
2015-10-26 paulson new lemmas about topology, etc., for Cauchy integral formula
2015-10-02 paulson New theorems about connected sets. And pairwise moved to Set.thy.
2015-09-30 paulson real_of_nat_Suc is now a simprule
2015-09-21 wenzelm isabelle update_cartouches;
2015-08-19 paulson New material and fixes related to the forthcoming Stone-Weierstrass development
2015-07-28 paulson tweaks. Got rid of a really slow step
2015-07-27 paulson New material for Cauchy's integral theorem
2015-07-20 paulson new material for multivariate analysis, etc.
2015-06-10 wenzelm isabelle update_cartouches;
2015-05-28 paulson Convex hulls: theorems about interior, etc. And a few simple lemmas.
2015-05-26 paulson New material about paths, and some lemmas
2015-04-30 paulson tidying some messy proofs
2015-04-28 paulson New material about complex transcendental functions (especially Ln, Arg) and polynomials
2015-03-31 paulson rationalised and generalised some theorems concerning abs and x^2.
2015-02-19 haftmann establish unique preferred fact names
2014-11-02 wenzelm modernized header;
2014-07-05 haftmann prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann reduced name variants for assoc and commute on plus and mult
2014-06-28 haftmann fact consolidation
2014-04-11 nipkow made mult_nonneg_nonneg a simp rule
2014-04-09 hoelzl field_simps: better support for negation and division, and power
2014-04-09 hoelzl revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
2014-04-06 wenzelm tuned proofs;
2014-04-03 paulson removing simprule status for divide_minus_left and divide_minus_right
2014-03-18 huffman remove unnecessary finiteness assumptions from lemmas about setsum
2014-03-16 haftmann normalising simp rules for compound operators
2014-03-04 huffman tuned proof
2014-02-27 paulson A bit of tidying up
2014-01-25 wenzelm tuned proof;
2013-12-16 immler summarized notions related to ordered_euclidean_space and intervals in separate theory
2013-12-16 immler introduced ordered real vector spaces
2013-12-16 immler ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
2013-12-09 wenzelm more antiquotations;
2013-11-19 haftmann eliminiated neg_numeral in favour of - (numeral _)
2013-11-12 hoelzl add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
2013-11-01 haftmann more simplification rules on unary and binary minus
2013-09-26 huffman tuned proofs
2013-09-26 huffman moved lemma
2013-09-24 wenzelm tuned proofs;
2013-09-18 wenzelm tuned proofs;
2013-09-13 huffman make 'linear' into a sublocale of 'bounded_linear';
2013-09-12 huffman new lemmas
2013-09-12 huffman prefer theorem name over 'long_thm_list(n)'
less more (0) -60 tip