| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
explicit equivalence for strict order on lattices
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 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
|
| Wed, 10 Oct 2012 12:52:24 +0200 |
haftmann |
more explicit code equations
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:41:11 +0100 |
noschinl |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 15:11:24 +0100 |
noschinl |
tuned simpset
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 20:10:14 +0100 |
haftmann |
tuned syntax declarations; tuned structure
|
file |
diff |
annotate
|
| Sun, 26 Feb 2012 15:28:48 +0100 |
haftmann |
marked candidates for rule declarations
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 20:33:35 +0100 |
haftmann |
moved lemmas for orderings and lattices on predicates to corresponding theories, retaining declaration order of classical rules; tuned headings; tuned syntax
|
file |
diff |
annotate
|
| Tue, 21 Feb 2012 08:15:42 +0100 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
| Sun, 19 Feb 2012 15:30:35 +0100 |
haftmann |
distributed lattice properties of predicates to places of instantiation
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 16:22:01 +0200 |
noschinl |
tune proofs
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 16:21:48 +0200 |
noschinl |
tune simpset for Complete_Lattices
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 22:33:36 +0200 |
haftmann |
move legacy candiates to bottom; marked candidates for default simp rules
|
file |
diff |
annotate
|