| Wed, 02 Oct 2013 16:29:40 +0200 |
blanchet |
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
|
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
|
| Sat, 28 Sep 2013 22:47:17 +0200 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 00:01:10 +0200 |
blanchet |
register codatatypes with Nitpick
|
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
|
| Tue, 17 Sep 2013 01:09:51 +0200 |
blanchet |
return right theorems
|
file |
diff |
annotate
|
| Fri, 13 Sep 2013 02:26:59 +0200 |
blanchet |
don't wrongly destroy sum types in coiterators
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 14:22:11 +0200 |
blanchet |
include map theorems in datastructure for "primcorec"
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 13:47:58 +0200 |
blanchet |
enriched data structure with necessary theorems
|
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
|