| Tue, 21 Oct 2014 17:23:11 +0200 |
desharna |
move theorem 'rec_o_map'
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 16:17:36 +0200 |
desharna |
generate 'sel_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:57 +0200 |
desharna |
add 'fp_bnf' to 'bnf_sugar'
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:56 +0200 |
desharna |
preserve the structure of 'set_intros' theorem in ML
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:54 +0200 |
desharna |
preserve the structure of 'map_sel' theorem in ML
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:11:35 +0200 |
desharna |
preserve the structure of 'set_sel' theorem in ML
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:48 +0200 |
desharna |
add 'set_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:47 +0200 |
desharna |
add 'common_set_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:42 +0200 |
desharna |
add 'rel_co_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:29 +0200 |
desharna |
add 'common_rel_co_induct' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:15 +0200 |
desharna |
add 'co_rec_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:03 +0200 |
desharna |
add 'co_rec_disc_iffs' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:49 +0200 |
desharna |
add 'disc_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:39 +0200 |
desharna |
add 'case_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:24 +0200 |
desharna |
add 'ctr_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:12 +0200 |
desharna |
add 'set_cases' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:04 +0200 |
desharna |
add 'set_intros' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:45 +0200 |
desharna |
add 'set_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:36 +0200 |
desharna |
add 'set_thms' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:24 +0200 |
desharna |
add 'rel_cases' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:15 +0200 |
desharna |
add 'rel_intros' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:04 +0200 |
desharna |
add 'rel_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:32:53 +0200 |
desharna |
add 'map_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:32:41 +0200 |
desharna |
add 'map_disc_iffs' to 'fp_sugar'
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:28 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:26 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:54 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:15 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:08 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:36:54 +0200 |
desharna |
refactor fp_sugar with empty substructures
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 12:11:41 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 10:49:07 +0200 |
blanchet |
generate 'code' attribute only if 'code' plugin is enabled
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 23:54:39 +0200 |
blanchet |
proper checks -- the calls data structure may contain spurious entries
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
more canonical (and correct) local theory threading
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 19:21:19 +0200 |
blanchet |
made N2M work with sort constraints (cf. TODO)
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 19:21:07 +0200 |
blanchet |
honour sorts in N2M
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:35 +0200 |
blanchet |
improved caching
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 19:28:00 +0200 |
blanchet |
drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
more compatibility between old- and new-style datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:47 +0200 |
blanchet |
made transfer functions slightly more general
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:48:59 +0200 |
blanchet |
improved unfolding of 'let's
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:48:59 +0200 |
blanchet |
less aggressive unfolding; removed debugging;
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 17:01:49 +0200 |
desharna |
generate 'corec_code' theorem for codatatypes
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
tuned variable names
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
no need to make 'size' generation an interpretation -- overkill
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
manual merge + added 'rel_distincts' field to record for symmetry
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
generate size instances for new-style datatypes
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:16 +0200 |
kuncar |
export theorems
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 18:40:21 +0200 |
blanchet |
generate cliques for 'prim(co)rec' N2M
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 18:22:11 +0200 |
blanchet |
thread mutual cliques through
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 01:02:21 +0100 |
blanchet |
balance tuples that represent curried functions
|
file |
diff |
annotate
|