| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
explicit distributivity facts on min/max
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 15:52:25 +0100 |
haftmann |
postponed min/max lemmas until abstract lattice is available
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 15:52:25 +0100 |
haftmann |
prefer abstract simp rule
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 10:09:43 +0100 |
haftmann |
more lemmas on abstract lattices
|
file |
diff |
annotate
|
| Tue, 24 Dec 2013 11:24:16 +0100 |
haftmann |
tuning and augmentation of min/max lemmas;
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
rationalize imports
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
examples for interpretation into target
|
file |
diff |
annotate
|
| Mon, 01 Apr 2013 17:42:29 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 21:53:56 +0100 |
haftmann |
more uniform style for interpretation and sublocale declarations
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:49:57 +0100 |
haftmann |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 17:11:06 +0100 |
haftmann |
locales for abstract orders
|
file |
diff |
annotate
|
| Sun, 10 Mar 2013 14:36:03 +0100 |
nipkow |
stepwise instantiation is more modular
|
file |
diff |
annotate
|
| Sat, 22 Dec 2012 00:04:50 +0100 |
nipkow |
added simp rule
|
file |
diff |
annotate
|