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