| 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
|
| Thu, 06 May 2010 23:11:57 +0200 |
haftmann |
former free-floating field_comp_conv now in structure Normalizer
|
file |
diff |
annotate
|
| Mon, 03 May 2010 10:28:19 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
| Sat, 01 May 2010 07:35:22 -0700 |
huffman |
move setsum lemmas to Product_plus.thy
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:35:10 +0200 |
hoelzl |
Moved Convex theory to library.
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 07:22:01 -0700 |
huffman |
remove redundant constants pastecart, fstcart, sndcart; users should prefer Pair, fst, snd instead
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 22:02:55 -0700 |
huffman |
remove redundant lemma norm_0
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:11:07 -0700 |
huffman |
move path-related stuff into new theory file
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 11:03:04 -0700 |
huffman |
generalize types of path operations
|
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
|
| 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
|
| Sun, 25 Apr 2010 10:23:03 -0700 |
huffman |
generalize more constants and lemmas
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 09:01:03 -0700 |
huffman |
simplify types of path operations (use real instead of real^1)
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 07:41:57 -0700 |
huffman |
add lemmas convex_real_interval and convex_box
|
file |
diff |
annotate
|