src/HOL/Multivariate_Analysis/Determinants.thy
2016-07-13 paulson 2016-07-13 lots of new theorems about differentiable_on, retracts, ANRs, etc.
2016-05-27 wenzelm 2016-05-27 tuned proofs, to allow unfold_abs_def;
2016-05-09 paulson 2016-05-09 lemmas about dimension, hyperplanes, span, etc.
2016-04-04 paulson 2016-04-04 Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
2016-02-25 paulson 2016-02-25 Conformal_mappings: a big development in complex analysis (+ some lemmas)
2015-09-30 paulson 2015-09-30 Dead wood removal
2015-06-10 wenzelm 2015-06-10 isabelle update_cartouches;
2015-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
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-05-30 hoelzl 2014-05-30 introduce more powerful reindexing rules for big operators
2014-04-12 haftmann 2014-04-12 more operations and lemmas
2014-03-18 huffman 2014-03-18 remove unnecessary finiteness assumptions from lemmas about setsum
2013-09-24 wenzelm 2013-09-24 tuned proofs;
2013-09-12 huffman 2013-09-12 make 'linear' into a sublocale of 'bounded_linear'; replace 'linear_def' with 'linear_iff'
2013-08-28 wenzelm 2013-08-28 tuned proofs;
2013-08-18 wenzelm 2013-08-18 more symbols;
2013-06-25 Stephen W. Nuchia 2013-06-25 Generalize trace_mult_sym to square products of non-square matrices.
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
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-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-08-23 huffman 2011-08-23 declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;
2011-08-17 huffman 2011-08-17 Determinants.thy: avoid using mem_def/Collect_def
2011-08-16 huffman 2011-08-16 get Multivariate_Analysis/Determinants.thy compiled and working again
2011-03-13 wenzelm 2011-03-13 tuned headers;
2010-10-24 nipkow 2010-10-24 nat_number -> eval_nat_numeral
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-04-29 huffman 2010-04-29 define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
2010-04-28 huffman 2010-04-28 generalize some euclidean space lemmas
2010-04-27 huffman 2010-04-27 merged
2010-04-26 huffman 2010-04-26 move definitions and theorems for type real^1 to separate theory file
2010-04-27 haftmann 2010-04-27 merged
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 huffman 2010-04-26 merged
2010-04-26 huffman 2010-04-26 fix lots of looping simp calls and other warnings
2010-04-26 haftmann 2010-04-26 dropped group_simps, ring_simps, field_eq_simps
2010-03-02 himmelma 2010-03-02 replaced \<bullet> with inner
2010-02-16 hoelzl 2010-02-16 Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-07 hoelzl 2010-01-07 finite annotation on cartesian product is now implicit.
2010-01-06 himmelma 2010-01-06 Made finite cartesian products finite
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis