src/HOL/Multivariate_Analysis/Determinants.thy
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Fri, 30 May 2014 14:55:10 +0200 hoelzl introduce more powerful reindexing rules for big operators
Sat, 12 Apr 2014 11:27:36 +0200 haftmann more operations and lemmas
Tue, 18 Mar 2014 09:39:07 -0700 huffman remove unnecessary finiteness assumptions from lemmas about setsum
Tue, 24 Sep 2013 21:23:40 +0200 wenzelm tuned proofs;
Thu, 12 Sep 2013 18:09:17 -0700 huffman make 'linear' into a sublocale of 'bounded_linear';
Wed, 28 Aug 2013 23:41:21 +0200 wenzelm tuned proofs;
Sun, 18 Aug 2013 19:59:19 +0200 wenzelm more symbols;
Tue, 25 Jun 2013 17:13:09 -0500 Stephen W. Nuchia Generalize trace_mult_sym to square products of non-square matrices.
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Tue, 23 Aug 2011 14:11:02 -0700 huffman declare euclidean_simps [simp] at the point they are proved;
Wed, 17 Aug 2011 15:02:17 -0700 huffman Determinants.thy: avoid using mem_def/Collect_def
Tue, 16 Aug 2011 07:56:17 -0700 huffman get Multivariate_Analysis/Determinants.thy compiled and working again
Sun, 13 Mar 2011 22:55:50 +0100 wenzelm tuned headers;
Sun, 24 Oct 2010 20:19:00 +0200 nipkow nat_number -> eval_nat_numeral
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Mon, 21 Jun 2010 19:33:51 +0200 hoelzl Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
Thu, 29 Apr 2010 11:41:04 -0700 huffman 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
Wed, 28 Apr 2010 21:39:14 -0700 huffman generalize some euclidean space lemmas
Tue, 27 Apr 2010 11:17:50 -0700 huffman merged
Mon, 26 Apr 2010 12:19:57 -0700 huffman move definitions and theorems for type real^1 to separate theory file
Tue, 27 Apr 2010 08:18:25 +0200 haftmann merged
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 09:45:22 -0700 huffman merged
Mon, 26 Apr 2010 09:21:25 -0700 huffman fix lots of looping simp calls and other warnings
Mon, 26 Apr 2010 11:34:19 +0200 haftmann dropped group_simps, ring_simps, field_eq_simps
Tue, 02 Mar 2010 21:32:37 +0100 himmelma replaced \<bullet> with inner
Tue, 16 Feb 2010 15:16:33 +0100 hoelzl Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Thu, 07 Jan 2010 18:56:39 +0100 hoelzl finite annotation on cartesian product is now implicit.
Wed, 06 Jan 2010 13:07:30 +0100 himmelma Made finite cartesian products finite
Fri, 23 Oct 2009 13:23:18 +0200 himmelma distinguished session for multivariate analysis
less more (0) tip