| 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
|