| Tue, 06 Oct 2009 18:44:06 +0200 |
haftmann |
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 17:23:00 +0200 |
haftmann |
moved lemmas about sup on bool to Lattices.thy
|
file |
diff |
annotate
|
| Wed, 30 Sep 2009 17:04:21 +0200 |
haftmann |
tuned headings
|
file |
diff |
annotate
|
| Fri, 25 Sep 2009 09:50:31 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:32:53 +0200 |
haftmann |
removed potentially dangerous rules from pred_set_conv
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added first prototype of the extended predicate compiler
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 09:07:48 +0200 |
haftmann |
be more cautious wrt. simp rules: sup1_iff, sup2_iff, inf1_iff, inf2_iff, SUP1_iff, SUP2_iff, INF1_iff, INF2_iff are no longer simp by default
|
file |
diff |
annotate
|
| Tue, 15 Sep 2009 19:16:35 +0200 |
haftmann |
hide new constants
|
file |
diff |
annotate
|
| Tue, 15 Sep 2009 12:11:10 +0200 |
haftmann |
added emptiness check predicate and singleton projection
|
file |
diff |
annotate
|
| Fri, 14 Aug 2009 15:36:54 +0200 |
haftmann |
formally stylized
|
file |
diff |
annotate
|
| Mon, 27 Jul 2009 21:47:41 +0200 |
krauss |
"more standard" argument order of relation composition (op O)
|
file |
diff |
annotate
|
| Fri, 03 Jul 2009 16:51:06 +0200 |
haftmann |
avoid useless code equations
|
file |
diff |
annotate
|
| Thu, 21 May 2009 09:07:13 +0200 |
haftmann |
added Predicate.map in SML environment
|
file |
diff |
annotate
|
| Wed, 20 May 2009 22:24:07 +0200 |
haftmann |
added Predicate.map
|
file |
diff |
annotate
|
| Wed, 13 May 2009 18:41:36 +0200 |
haftmann |
dropped sort constraint on predicate equality
|
file |
diff |
annotate
|
| Tue, 12 May 2009 17:09:35 +0200 |
haftmann |
added dummy values keyword
|
file |
diff |
annotate
|
| Mon, 11 May 2009 19:54:24 +0200 |
haftmann |
avoid latex output problem
|
file |
diff |
annotate
|
| Mon, 11 May 2009 17:20:52 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Mon, 11 May 2009 09:18:42 +0200 |
bulwahn |
Added pred_code command
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 11:10:23 +0200 |
bulwahn |
added general preprocessing of equality in predicates for code generation
|
file |
diff |
annotate
|
| Wed, 22 Apr 2009 19:09:19 +0200 |
haftmann |
fixed compilation of predicate types in ML environment
|
file |
diff |
annotate
|
| Fri, 17 Apr 2009 15:14:06 +0200 |
haftmann |
static compilation of enumeration type
|
file |
diff |
annotate
|
| 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
|