| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
tuning
|
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
|
| Fri, 26 Sep 2014 14:35:09 +0200 |
desharna |
add attribute 'case_names' to 'set_case'
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:56 +0200 |
desharna |
generate 'corec_transfer' for codatatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 21:00:07 +0200 |
blanchet |
avoid type variable name clash
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 21:00:07 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 18:12:09 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 17:56:37 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 16:34:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 11:17:44 +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
|
| Sat, 13 Sep 2014 18:08:38 +0200 |
blanchet |
imported patch phantoms
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 13:50:55 +0200 |
desharna |
refactor repeated terms in a single variable
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 13:50:51 +0200 |
desharna |
make 'ctr_transfer' tactic more robust
|
file |
diff |
annotate
|
| Fri, 12 Sep 2014 13:48:15 +0200 |
desharna |
make 'rel_sel' and 'map_sel' tactics more robust
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 23:54:47 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
avoid duplicate case names
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
preserve case names in '(co)induct' theorems generated by prim(co)rec'
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
set 'fundef_cong' attribute also for (co)datatypes with no live type variables
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
prevent infinite loop when type variables are of a non-'type' sort
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 19:21:07 +0200 |
blanchet |
honour sorts in N2M
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 16:51:35 +0200 |
blanchet |
proper sort constraints in map and rel theorems
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 16:09:10 +0200 |
blanchet |
made code work also in the presence of deads
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
properly note theorems for split recursors
|
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
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
export one more ML function
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
introduced mechanism to filter interpretations
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
fixed infinite loops in 'register' functions + more uniform API
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:00 +0200 |
blanchet |
centralized and cleaned up naming handling
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 11:20:59 +0200 |
blanchet |
tweaked setup for datatype realizer
|
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
|
| Wed, 03 Sep 2014 22:49:05 +0200 |
blanchet |
introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 22:47:35 +0200 |
blanchet |
tuned BNF database handling
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:31:37 +0200 |
blanchet |
tuning
|
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 |
added theory-based getters for convenience
|
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, 01 Sep 2014 13:23:39 +0200 |
desharna |
generate 'rel_transfer' for BNFs
|
file |
diff |
annotate
|
| Fri, 29 Aug 2014 14:36:51 +0200 |
desharna |
generate 'disc_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Fri, 29 Aug 2014 14:21:24 +0200 |
desharna |
generate 'case_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Wed, 27 Aug 2014 13:05:59 +0200 |
blanchet |
removed not so interesting 'set_empty'
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 16:46:31 +0200 |
desharna |
generate 'ctr_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 19:16:30 +0200 |
blanchet |
set attributes on 'set_cases' theorem
|
file |
diff |
annotate
|