Tue, 04 Sep 2012 23:09:08 +0200 |
blanchet |
optionally provide extra dead variables to the FP constructions
|
file |
diff |
annotate
|
Tue, 04 Sep 2012 21:23:11 +0200 |
blanchet |
added robustness
|
file |
diff |
annotate
|
Tue, 04 Sep 2012 18:49:40 +0200 |
blanchet |
implemented "mk_case_tac" -- and got rid of "cheat_tac"
|
file |
diff |
annotate
|
Tue, 04 Sep 2012 18:14:58 +0200 |
blanchet |
define "case" constant
|
file |
diff |
annotate
|
Tue, 04 Sep 2012 17:23:08 +0200 |
blanchet |
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
|
file |
diff |
annotate
|
Tue, 04 Sep 2012 15:51:32 +0200 |
blanchet |
implemented "mk_exhaust_tac"
|
file |
diff |
annotate
|
Tue, 04 Sep 2012 13:05:01 +0200 |
blanchet |
more work on FP sugar
|
file |
diff |
annotate
|
Tue, 04 Sep 2012 13:02:32 +0200 |
blanchet |
more work on FP sugar
|
file |
diff |
annotate
|
Mon, 03 Sep 2012 11:54:21 +0200 |
blanchet |
rearrange dependencies
|
file |
diff |
annotate
|
Thu, 30 Aug 2012 09:47:46 +0200 |
blanchet |
more work on BNF sugar -- up to derivation of nchotomy
|
file |
diff |
annotate
|
Thu, 30 Aug 2012 09:47:46 +0200 |
blanchet |
more work on BNF sugar
|
file |
diff |
annotate
|
Tue, 28 Aug 2012 17:16:00 +0200 |
blanchet |
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
|
file |
diff |
annotate
|