| Thu, 14 Nov 2013 20:55:09 +0100 |
blanchet |
fixed type variable confusion in 'datatype_new_compat'
|
file |
diff |
annotate
|
| Thu, 07 Nov 2013 00:37:18 +0100 |
blanchet |
properly detect when to perform n2m -- e.g. handle the case of two independent functions on irrelevant types being defined in parallel
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 12:40:58 +0100 |
blanchet |
use right permutation in 'map2'
|
file |
diff |
annotate
|
| Mon, 21 Oct 2013 09:14:05 +0200 |
blanchet |
warn about incompatible recursor signature
|
file |
diff |
annotate
|
| Wed, 02 Oct 2013 10:53:15 +0200 |
blanchet |
tuned command descriptions
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 14:13:24 +0200 |
blanchet |
got rid of dead feature
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 14:05:25 +0200 |
blanchet |
renamed theory file
|
file |
diff |
annotate
|
| Mon, 30 Sep 2013 22:36:43 +0200 |
blanchet |
made SML/NJ happy
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 01:05:07 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 00:01:10 +0200 |
blanchet |
register codatatypes with Nitpick
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 12:04:48 +0200 |
blanchet |
took out spurious attributes (no need for several code equations / simps for thesame constants)
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 11:44:30 +0200 |
blanchet |
have "datatype_new_compat" register induction and recursion theorems in nested case
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 12:12:41 +0200 |
blanchet |
renamed command to clarify connection with BNF
|
file |
diff |
annotate
|
| Fri, 30 Aug 2013 11:27:23 +0200 |
blanchet |
moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
|
file |
diff |
annotate
|