| Mon, 06 Oct 2014 13:33:45 +0200 |
desharna |
add 'set_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:36 +0200 |
desharna |
add 'set_thms' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:24 +0200 |
desharna |
add 'rel_cases' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:15 +0200 |
desharna |
add 'rel_intros' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:33:04 +0200 |
desharna |
add 'rel_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:32:53 +0200 |
desharna |
add 'map_sels' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:32:41 +0200 |
desharna |
add 'map_disc_iffs' to 'fp_sugar'
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:28 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:43:26 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:54 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:15 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:41:08 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
| Fri, 26 Sep 2014 14:36:54 +0200 |
desharna |
refactor fp_sugar with empty substructures
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:56 +0200 |
desharna |
generate 'corec_transfer' for codatatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved old 'size' generator together with 'old_datatype'
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
tuned fact visibility
|
file |
diff |
annotate
|
| Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|
file |
diff |
annotate
|