| Thu, 29 Apr 2010 15:00:40 +0200 |
haftmann |
code_reflect: specify module name directly after keyword
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:56:18 +0200 |
haftmann |
avoid code_datatype antiquotation
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 12:49:14 -0700 |
huffman |
add/change some lemmas about lattices
|
file |
diff |
annotate
|
| Fri, 11 Dec 2009 14:43:56 +0100 |
haftmann |
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
|
file |
diff |
annotate
|
| Sat, 05 Dec 2009 20:02:21 +0100 |
haftmann |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 18:19:30 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 08:25:53 +0100 |
bulwahn |
adding derived constant Predicate.holds to Predicate theory; adopting the predicate compiler
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 09:10:37 +0100 |
bulwahn |
removed dummy setup for predicate compiler commands as the compiler is now part of HOL-Main
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 09:02:20 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
developing an executable the operator
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
generalizing singleton with a default value
|
file |
diff |
annotate
|
| Sat, 24 Oct 2009 16:54:32 +0200 |
bulwahn |
moved meta_fun_cong lemma into ML-file; tuned
|
file |
diff |
annotate
|
| 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
|