| Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
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
|
| Sun, 04 Jul 2010 09:26:30 -0700 |
huffman |
generalize some lemmas about derivatives
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 21:29:58 -0700 |
huffman |
generalize some lemmas about derivatives
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 19:00:15 -0700 |
huffman |
generalize more euclidean_space lemmas
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 15:32:26 +0200 |
haftmann |
inner_simps is not enough, need also local facts
|
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
|
| Tue, 11 May 2010 19:21:05 +0200 |
hoelzl |
Removed usage of normalizating locales.
|
file |
diff |
annotate
|
| Fri, 07 May 2010 09:59:24 +0200 |
haftmann |
prefix normalizing replaces class_semiring
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:11:57 +0200 |
haftmann |
former free-floating field_comp_conv now in structure Normalizer
|
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 22:20:59 -0700 |
huffman |
remove redundant lemma vector_dist_norm
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 15:05:45 -0700 |
huffman |
move operator norm stuff to new theory file
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 16:28:58 -0700 |
huffman |
more lemmas to Vec1.thy
|
file |
diff |
annotate
|