| Wed, 20 Nov 2013 20:45:20 +0100 | blanchet | moved 'coinduction' proof method to 'HOL' | file | diff | annotate |
| Tue, 19 Nov 2013 14:33:20 +0100 | blanchet | case_if -> case_eq_if + docs | file | diff | annotate |
| Thu, 14 Nov 2013 20:55:09 +0100 | blanchet | fixed type variable confusion in 'datatype_new_compat' | file | diff | annotate |
| Tue, 12 Nov 2013 13:47:24 +0100 | blanchet | tuned headers | file | diff | annotate |
| Tue, 12 Nov 2013 13:47:24 +0100 | blanchet | moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction | file | diff | annotate | base |