| Tue, 02 Oct 2012 01:00:18 +0200 |
blanchet |
continued changing type of corec type
|
file |
diff |
annotate
|
| Tue, 02 Oct 2012 01:00:18 +0200 |
blanchet |
made (co)rec tactic more robust when the simplifier succeeds early
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 11:04:30 +0200 |
blanchet |
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 10:46:30 +0200 |
blanchet |
tweaked corecursor/coiterator tactic
|
file |
diff |
annotate
|
| Mon, 01 Oct 2012 10:34:58 +0200 |
blanchet |
changed the type of the recursor for nested recursion
|
file |
diff |
annotate
|
| Sun, 30 Sep 2012 22:02:34 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 30 Sep 2012 12:04:13 +0200 |
traytel |
tuned tactic
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:23:32 +0200 |
blanchet |
simplified simpset
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 15:14:11 +0200 |
blanchet |
fixed simplification of prod and sum relators to avoid issues with e.g. codata ('a, 'b) k = K "'a + 'b"
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 11:31:51 +0200 |
traytel |
tuned tactic
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 09:38:07 +0200 |
traytel |
tuned tactic
|
file |
diff |
annotate
|
| Fri, 28 Sep 2012 09:12:50 +0200 |
blanchet |
renamed ML file in preparation for next step
|
file |
diff |
annotate
| base
|