| 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
|
| Wed, 17 Sep 2014 12:09:33 +0200 |
blanchet |
tweaked compatibility layer
|
file |
diff |
annotate
|
| Wed, 17 Sep 2014 08:23:53 +0200 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
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 18:54:36 +0200 |
blanchet |
speed up old Nominal by killing type variables
|
file |
diff |
annotate
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 15:54:33 +0200 |
blanchet |
export right sorts
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:08 +0200 |
blanchet |
wildcards in plugins
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
improved 'datatype_compat' further for recursion through functions
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
no type-based lookup -- these fail in the general, ambiguous case
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:02 +0200 |
blanchet |
tuning
|
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 |
tuning
|
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
|
| 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 |
named interpretations
|
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 00:06:19 +0200 |
blanchet |
more compatibility functions
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:18 +0200 |
blanchet |
codatatypes are not datatypes
|
file |
diff |
annotate
|
| Tue, 02 Sep 2014 12:11:04 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 19:58:25 +0200 |
blanchet |
avoid more 'bad background theory' issues
|
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 18:42:02 +0200 |
blanchet |
ported to use new-style datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 17:34:03 +0200 |
blanchet |
ported Refute to use new datatypes when possible
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:34:38 +0200 |
blanchet |
added primrec compatibility function
|
file |
diff |
annotate
|