Wed, 05 Sep 2012 11:16:34 +0200 | blanchet | reindented code | file | diff | annotate |
Wed, 05 Sep 2012 11:08:18 +0200 | blanchet | fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case | file | diff | annotate |
Wed, 05 Sep 2012 00:58:54 +0200 | blanchet | fixed bugs in one-constructor case | file | diff | annotate |
Tue, 04 Sep 2012 13:05:07 +0200 | blanchet | renamed "disc_exclus" theorem to "disc_exclude" | file | diff | annotate |
Tue, 04 Sep 2012 13:02:31 +0200 | blanchet | renamed theorem | file | diff | annotate |
Tue, 04 Sep 2012 13:02:30 +0200 | blanchet | allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes) | file | diff | annotate |
Mon, 03 Sep 2012 11:54:21 +0200 | blanchet | rearrange dependencies | file | diff | annotate |
Mon, 03 Sep 2012 11:54:21 +0200 | blanchet | renamed three BNF/(co)datatype-related commands | file | diff | annotate | base |