| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 20:43:13 +0100 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 15:21:59 +0100 |
desharna |
fix 'unfla' function
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:12 +0200 |
desharna |
generate 'map_o_corec' for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:11 +0200 |
desharna |
move theorem 'rec_o_map'
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:23:10 +0200 |
desharna |
warn for not fully mutually (co)recursive types
|
file |
diff |
annotate
|
| Thu, 16 Oct 2014 11:56:46 +0200 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 16:17:36 +0200 |
desharna |
generate 'sel_transfer' for (co)datatypes
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 16:17:34 +0200 |
desharna |
add 'kind' to 'cr_sugar'
|
file |
diff |
annotate
|
| Tue, 14 Oct 2014 15:39:57 +0200 |
desharna |
add 'fp_bnf' to 'bnf_sugar'
|
file |
diff |
annotate
|
| 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 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Mon, 06 Oct 2014 13:42:48 +0200 |
desharna |
refactor 'map_sel_thms' and 'set_sel_thms'
|
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:40:02 +0200 |
desharna |
rename one of the two 'rel_eq_thms' to 'rel_code_thms'
|
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: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
|
| Thu, 02 Oct 2014 12:02:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 29 Sep 2014 10:39:39 +0200 |
blanchet |
tuning
|
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
|
| Fri, 26 Sep 2014 14:35:09 +0200 |
desharna |
add attribute 'case_names' to 'set_case'
|
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
|
| Wed, 24 Sep 2014 21:00:07 +0200 |
blanchet |
avoid type variable name clash
|
file |
diff |
annotate
|
| Wed, 24 Sep 2014 21:00:07 +0200 |
blanchet |
tuning
|
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
|
| Mon, 15 Sep 2014 18:12:09 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 17:56:37 +0200 |
blanchet |
refactoring
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 16:34:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 15 Sep 2014 11:17:44 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|