Tue, 04 Sep 2012 13:02:32 +0200 | blanchet | more work on FP sugar | changeset | files |
Tue, 04 Sep 2012 13:02:31 +0200 | blanchet | renamed theorem | changeset | files |
Tue, 04 Sep 2012 13:02:30 +0200 | blanchet | tuned TODO comment | changeset | files |
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) | changeset | files |
Tue, 04 Sep 2012 13:02:29 +0200 | blanchet | removed oddities | changeset | files |
Tue, 04 Sep 2012 13:02:28 +0200 | blanchet | allow "*" to indicate no discriminator | changeset | files |