| Fri, 13 Sep 2013 22:31:56 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 13 Sep 2013 22:16:26 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 20:34:45 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
|
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
|
| Thu, 01 Sep 2011 09:02:14 -0700 |
huffman |
modernize lemmas about 'continuous' and 'continuous_on';
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:41:38 -0700 |
huffman |
replace some continuous_on lemmas with more general versions
|
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
|
| Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 13:13:37 -0700 |
huffman |
more uniform naming scheme for finite cartesian product type and related theorems
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:24:10 +0100 |
wenzelm |
eliminated hard tabs;
|
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
|
| Thu, 01 Jul 2010 15:40:38 -0700 |
huffman |
convert theorem path_connected_sphere to euclidean_space class
|
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 16:11:07 -0700 |
huffman |
move path-related stuff into new theory file
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 15:22:03 -0700 |
huffman |
move proof of Fashoda meet theorem into separate file
|
file |
diff |
annotate
|