Tue, 04 Sep 2012 14:21:11 +0200 | blanchet | more work on FP sugar | changeset | files |
Tue, 04 Sep 2012 13:06:41 +0200 | blanchet | more work on sugar + simplify Trueprop + eq idiom everywhere | changeset | files |
Tue, 04 Sep 2012 13:05:07 +0200 | blanchet | renamed "disc_exclus" theorem to "disc_exclude" | changeset | files |
Tue, 04 Sep 2012 13:05:01 +0200 | blanchet | more work on FP sugar | changeset | files |
Tue, 04 Sep 2012 13:02:32 +0200 | blanchet | smarter "*" syntax -- fallback on "_" if "*" is impossible | changeset | files |
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 |