| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 00:36:01 +0100 |
hoelzl |
adapt proofs to changed set_plus_image (cf. ee8d0548c148);
|
file |
diff |
annotate
|
| Thu, 02 Dec 2010 16:45:28 +0100 |
hoelzl |
Prove rel_interior_convex_hull_union (by Grechuck Bogdan).
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 21:09:36 +0100 |
wenzelm |
keep private things private, without comments;
|
file |
diff |
annotate
|
| Fri, 05 Nov 2010 14:17:18 +0100 |
hoelzl |
Extend convex analysis by Bogdan Grechuk
|
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, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 09:14:51 -0700 |
huffman |
generalize type of is_interval to class euclidean_space
|
file |
diff |
annotate
|
| Thu, 01 Jul 2010 09:24:04 -0700 |
huffman |
generalize more lemmas from ordered_euclidean_space to euclidean_space
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 11:51:35 -0700 |
huffman |
minimize dependencies on Numeral_Type
|
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
|
| Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
| Fri, 07 May 2010 09:59:24 +0200 |
haftmann |
prefix normalizing replaces class_semiring
|
file |
diff |
annotate
|