| Fri, 30 Dec 2016 15:40:35 +0100 | blanchet | more uniform errors in '(prim)(co)rec(ursive)' variants | file | diff | annotate |
| Wed, 21 Dec 2016 12:49:15 +0100 | blanchet | generalized ML function (towards nonuniform datatypes) | file | diff | annotate |
| Mon, 12 Sep 2016 23:17:55 +0200 | blanchet | make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions | file | diff | annotate |
| Tue, 22 Mar 2016 12:39:37 +0100 | blanchet | put all 'bnf_*.ML' files together, irrespective of bootstrapping/dependency constraints | file | diff | annotate | base |