| Tue, 18 Mar 2014 15:53:48 +0100 |
hoelzl |
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:58 +0100 |
immler |
additional lemmas
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:58 +0100 |
immler |
removed dependencies on theory Ordered_Euclidean_Space
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 10:12:57 +0100 |
immler |
use cbox to relax class constraints
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 19:12:52 +0100 |
hoelzl |
unify syntax for has_derivative and differentiable
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 18:06:59 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 21:58:46 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
additional lemmas
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
remove redundant constants
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
prefer box over greaterThanLessThan on euclidean_space
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:52 +0100 |
hoelzl |
stronger inc_induct and dec_induct
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:45:02 +0100 |
hoelzl |
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:58 +0100 |
hoelzl |
use bdd_above and bdd_below for conditionally complete lattices
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 16:03:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 22:30:10 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 14 Sep 2013 13:59:57 +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
|
| Thu, 12 Sep 2013 09:39:02 -0700 |
huffman |
remove duplicate lemmas
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 00:00:59 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 23:50:03 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 18:14:47 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 00:18:30 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 23:11:02 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 07 Sep 2013 23:09:26 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2013 18:14:50 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|