| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
d945085c |
|
12-Sep-2016 |
blanchet <none@none> |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
| #
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
| #
057633fe |
|
14-Apr-2016 |
traytel <none@none> |
n2m operates on (un)folds
|
| #
049cf95c |
|
07-Apr-2016 |
traytel <none@none> |
(un)folds are not legacy
|
| #
1a96a7b9 |
|
05-Apr-2016 |
traytel <none@none> |
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
|
| #
4dd3178f |
|
27-Mar-2016 |
blanchet <none@none> |
added '_legacy' suffixes
|
| #
830f4f54 |
|
22-Mar-2016 |
traytel <none@none> |
document that n2m does not depend on most things in fp_sugar in its type
|
| #
97b25dd9 |
|
17-Feb-2016 |
blanchet <none@none> |
making 'pred_inject' a first-class BNF citizen
|
| #
2514dd4c |
|
15-Feb-2016 |
blanchet <none@none> |
keep 'ctor_iff_dtor' theorem around in BNF FP database
|
| #
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
| #
4930226f |
|
06-Sep-2015 |
haftmann <none@none> |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
| #
1426640f |
|
30-Mar-2015 |
blanchet <none@none> |
export more low-level theorems in data structure (partly for 'corec')
|
| #
955d0fc8 |
|
26-Mar-2015 |
blanchet <none@none> |
store low-level (un)fold constants
|
| #
23571538 |
|
07-Nov-2014 |
traytel <none@none> |
more complete fp_sugars for sum and prod;
tuned;
removed theorem duplicates;
removed obsolete Lifting_{Option,Product,Sum} theories
|
| #
824744a2 |
|
21-Oct-2014 |
desharna <none@none> |
generate 'map_o_corec' for (co)datatypes
* * *
document 'map_o_corec'
|
| #
686351a9 |
|
21-Oct-2014 |
desharna <none@none> |
move theorem 'rec_o_map'
* * *
move documentation of 'rec_o_map'
|
| #
f05f85f5 |
|
14-Oct-2014 |
desharna <none@none> |
generate 'sel_transfer' for (co)datatypes
|
| #
5ae17a36 |
|
14-Oct-2014 |
desharna <none@none> |
add 'fp_bnf' to 'bnf_sugar'
|
| #
9c060c90 |
|
14-Oct-2014 |
desharna <none@none> |
preserve the structure of 'set_intros' theorem in ML
|
| #
def076b7 |
|
14-Oct-2014 |
desharna <none@none> |
preserve the structure of 'map_sel' theorem in ML
|
| #
2be8af88 |
|
14-Oct-2014 |
desharna <none@none> |
preserve the structure of 'set_sel' theorem in ML
|
| #
ce27dd00 |
|
13-Oct-2014 |
wenzelm <none@none> |
tuned signature;
|
| #
9622cd51 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_rel_thms' to 'xtor_rels'
|
| #
191e6485 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_set_thmss' to 'xtor_setss'
|
| #
7d5fbd1c |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_map_thms' to 'xtor_maps'
|
| #
57c1cff0 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
|
| #
c54f4f14 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
|
| #
9665b67b |
|
06-Oct-2014 |
desharna <none@none> |
rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
|
| #
73c7c1b9 |
|
06-Oct-2014 |
desharna <none@none> |
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
|
| #
e364b08b |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_inducts' to 'fp_sugar'
|
| #
2cedfc03 |
|
06-Oct-2014 |
desharna <none@none> |
add 'common_set_inducts' to 'fp_sugar'
|
| #
467db70c |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_co_inducts' to 'fp_sugar'
|
| #
cadb7741 |
|
06-Oct-2014 |
desharna <none@none> |
add 'common_rel_co_induct' to 'fp_sugar'
|
| #
d76bbcfd |
|
06-Oct-2014 |
desharna <none@none> |
add 'co_rec_transfers' to 'fp_sugar'
|
| #
6d76dc50 |
|
06-Oct-2014 |
desharna <none@none> |
add 'co_rec_disc_iffs' to 'fp_sugar'
|
| #
8b25f959 |
|
06-Oct-2014 |
desharna <none@none> |
add 'disc_transfers' to 'fp_sugar'
|
| #
b0fae040 |
|
06-Oct-2014 |
desharna <none@none> |
add 'case_transfers' to 'fp_sugar'
|
| #
3fbae9a8 |
|
06-Oct-2014 |
desharna <none@none> |
add 'ctr_transfers' to 'fp_sugar'
|
| #
f5c26cc0 |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_cases' to 'fp_sugar'
|
| #
30cc7146 |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_intros' to 'fp_sugar'
|
| #
b5244d83 |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_sels' to 'fp_sugar'
|
| #
2ef889ae |
|
06-Oct-2014 |
desharna <none@none> |
add 'set_thms' to 'fp_sugar'
|
| #
3d17f9a3 |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_cases' to 'fp_sugar'
|
| #
58470965 |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_intros' to 'fp_sugar'
|
| #
24e3ec36 |
|
06-Oct-2014 |
desharna <none@none> |
add 'rel_sels' to 'fp_sugar'
|
| #
00bc7453 |
|
06-Oct-2014 |
desharna <none@none> |
add 'map_sels' to 'fp_sugar'
|
| #
4a7808d9 |
|
06-Oct-2014 |
desharna <none@none> |
add 'map_disc_iffs' to 'fp_sugar'
|
| #
906e82c7 |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
4434c5ed |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
9608121d |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
a14f7fdb |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
aa3cb8c8 |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar move theorems
|
| #
50b15776 |
|
26-Sep-2014 |
desharna <none@none> |
refactor fp_sugar with empty substructures
|
| #
eb1ed55c |
|
25-Sep-2014 |
desharna <none@none> |
generate 'corec_transfer' for codatatypes
|
| #
e05be41f |
|
25-Sep-2014 |
desharna <none@none> |
generate 'rec_transfer' for datatypes
|
| #
9b903e0e |
|
18-Sep-2014 |
blanchet <none@none> |
moved old 'size' generator together with 'old_datatype'
--HG--
rename : src/HOL/Tools/Function/old_size.ML => src/HOL/Tools/Old_Datatype/old_size.ML
|
| #
ffb23fae |
|
16-Sep-2014 |
blanchet <none@none> |
tuned fact visibility
|
| #
997718be |
|
16-Sep-2014 |
blanchet <none@none> |
register 'prod' and 'sum' as datatypes, to allow N2M through them
|