| Sun, 09 Sep 2012 10:15:58 +0200 | traytel | open typedef for datatypes | changeset | files |
| Sat, 08 Sep 2012 22:54:37 +0200 | blanchet | fixed and enabled iterator/recursor theorems | changeset | files |
| Sat, 08 Sep 2012 21:52:17 +0200 | blanchet | renamed for consistency | changeset | files |
| Sat, 08 Sep 2012 21:37:23 +0200 | blanchet | oops | changeset | files |
| Sat, 08 Sep 2012 21:33:15 +0200 | blanchet | tuning | changeset | files |
| Sat, 08 Sep 2012 21:30:31 +0200 | blanchet | for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants | changeset | files |
| Sat, 08 Sep 2012 21:21:27 +0200 | blanchet | fixed bug with one-value types with phantom type arguments | changeset | files |
| Sat, 08 Sep 2012 21:04:27 +0200 | blanchet | imported patch debugging | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | repaired "nofail4" example | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | renamed xxxBNF to pre_xxx | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | fixed handling of map of "fun" | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | comment out code that's not ready | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | tuning | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | construct the right iterator theorem in the recursive case | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | some work on coiter tactic | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | more sugar on codatatypes | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | define corecursors | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | define coiterators | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | TODO | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | tuning | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | completed iter/rec proofs | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | TODOs | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | implemented "mk_iter_or_rec_tac" | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | generate iter/rec goals | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | repaired constant types | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | some work towards iterator and recursor properties | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | tuning | changeset | files |
| Sat, 08 Sep 2012 21:04:26 +0200 | blanchet | correctly curry recursor arguments | changeset | files |