| Wed, 11 Mar 2009 08:45:47 +0100 |
haftmann |
explicit code equations for some rarely used pred operations
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 09:34:39 +0100 |
haftmann |
dropped eq_pred
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 15:25:29 +0100 |
haftmann |
refined enumeration implementation
|
file |
diff |
annotate
|
| Fri, 06 Mar 2009 20:30:17 +0100 |
haftmann |
added enumeration of predicates
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:39 +0200 |
berghofe |
- Added mem_def and predicate1I in some of the proofs
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:29 +0200 |
haftmann |
Sup now explicit parameter of complete_lattice
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:07:57 +0200 |
berghofe |
- Moved infrastructure for converting between sets and predicates
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:49 +0200 |
haftmann |
clarified import
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Sat, 10 Mar 2007 16:23:28 +0100 |
berghofe |
Generalized version of SUP and INF (with index set).
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:25:39 +0100 |
berghofe |
New theory for converting between predicates and sets.
|
file |
diff |
annotate
|