| Tue, 14 Oct 2014 15:39:56 +0200 |
desharna |
preserve the structure of 'set_intros' theorem in ML
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:54 +0200 |
desharna |
preserve the structure of 'map_sel' theorem in ML
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:11:35 +0200 |
desharna |
preserve the structure of 'set_sel' theorem in ML
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:41:37 +0200 |
desharna |
rename 'xtor_rel_thms' to 'xtor_rels'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:56 +0200 |
desharna |
rename 'xtor_set_thmss' to 'xtor_setss'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:40:31 +0200 |
desharna |
rename 'xtor_map_thms' to 'xtor_maps'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:39:12 +0200 |
desharna |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:40 +0200 |
desharna |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:38:13 +0200 |
desharna |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:37:38 +0200 |
desharna |
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:48 +0200 |
desharna |
add 'set_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:47 +0200 |
desharna |
add 'common_set_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:36:42 +0200 |
desharna |
add 'rel_co_inducts' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:29 +0200 |
desharna |
add 'common_rel_co_induct' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:15 +0200 |
desharna |
add 'co_rec_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:35:03 +0200 |
desharna |
add 'co_rec_disc_iffs' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:49 +0200 |
desharna |
add 'disc_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:39 +0200 |
desharna |
add 'case_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:24 +0200 |
desharna |
add 'ctr_transfers' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:12 +0200 |
desharna |
add 'set_cases' to 'fp_sugar'
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:34:04 +0200 |
desharna |
add 'set_intros' to 'fp_sugar'
|
file |
diff |
annotate
|
| 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
|