Mon, 23 Sep 2013 10:58:37 +0200 |
blanchet |
note coinduct theorems in "primcorec"
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 10:45:26 +0200 |
blanchet |
generate "simps" from "primcorec"
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 10:38:23 +0200 |
blanchet |
undid copy-paste
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 10:34:10 +0200 |
blanchet |
avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)
|
file |
diff |
annotate
|
Mon, 23 Sep 2013 10:30:43 +0200 |
blanchet |
tuned code
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 16:32:27 +0200 |
blanchet |
renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
|
file |
diff |
annotate
|
Fri, 20 Sep 2013 00:08:42 +0200 |
blanchet |
setting the stage for safe constructor simp rules
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 23:54:54 +0200 |
blanchet |
added TODO
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 17:38:03 +0200 |
traytel |
don't declare ctr view primcorec theorems as simp (they loop)
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 16:12:43 +0200 |
panny |
simplified code; eliminated some dummyTs
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 12:20:12 +0200 |
blanchet |
avoid infinite loop for unapplied terms + tuning
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 11:27:32 +0200 |
blanchet |
generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 01:09:25 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
Thu, 19 Sep 2013 00:32:33 +0200 |
panny |
generate more theorems (e.g. for types with only one constructor)
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 22:59:11 +0200 |
panny |
generate constructor view theorems
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 18:12:40 +0200 |
blanchet |
tuned tactics
|
file |
diff |
annotate
|
Wed, 18 Sep 2013 15:33:32 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 16 Sep 2013 15:03:23 +0200 |
panny |
prove simp theorems for newly generated definitions
|
file |
diff |
annotate
|
Thu, 05 Sep 2013 01:58:48 +0200 |
panny |
support indirect corecursion
|
file |
diff |
annotate
|
Wed, 04 Sep 2013 02:11:50 +0200 |
panny |
various refactoring;
|
file |
diff |
annotate
|
Mon, 02 Sep 2013 15:13:00 +0200 |
panny |
handle direct corecursion
|
file |
diff |
annotate
|
Sun, 01 Sep 2013 14:00:05 +0200 |
panny |
improved interfaces
|
file |
diff |
annotate
|
Sun, 01 Sep 2013 10:45:54 +0200 |
panny |
simplified rewriting of map arguments
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 23:55:03 +0200 |
traytel |
merged
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 23:49:14 +0200 |
traytel |
honor mixfix specifications
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 20:37:31 +0200 |
panny |
simplified recursive calls' replacement
|
file |
diff |
annotate
|
Sat, 31 Aug 2013 18:18:33 +0200 |
panny |
handle selector formulae with no corecursive calls
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 21:43:15 +0200 |
panny |
fixed bug in primrec_new (allow indirect recursion through constructor arguments other than the first)
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 14:17:19 +0200 |
blanchet |
more canonical naming
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 12:37:03 +0200 |
blanchet |
moved keywords down the hierarchy
|
file |
diff |
annotate
|
Fri, 30 Aug 2013 11:37:22 +0200 |
blanchet |
polished newly included files after moving
|
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
|