src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-06 traytel 2015-10-06 collect the names from goals in favor of fragile exports
2015-09-06 haftmann 2015-09-06 prefer "uncurry" as canonical name for case distinction on products in combinatorial view
2015-03-10 blanchet 2015-03-10 tuning
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-24 blanchet 2014-11-24 improved message in 'co' case
2014-11-08 wenzelm 2014-11-08 proper Envir.norm_type for result of Type.raw_unifys;
2014-10-21 desharna 2014-10-21 generate 'map_o_corec' for (co)datatypes * * * document 'map_o_corec'
2014-10-21 desharna 2014-10-21 move theorem 'rec_o_map' * * * move documentation of 'rec_o_map'
2014-10-14 desharna 2014-10-14 generate 'sel_transfer' for (co)datatypes
2014-10-14 desharna 2014-10-14 add 'fp_bnf' to 'bnf_sugar'
2014-10-14 desharna 2014-10-14 preserve the structure of 'set_intros' theorem in ML
2014-10-14 desharna 2014-10-14 preserve the structure of 'map_sel' theorem in ML
2014-10-14 desharna 2014-10-14 preserve the structure of 'set_sel' theorem in ML
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-10-06 desharna 2014-10-06 add 'set_inducts' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'common_set_inducts' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'rel_co_inducts' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'common_rel_co_induct' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'co_rec_transfers' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'co_rec_disc_iffs' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'disc_transfers' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'case_transfers' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'ctr_transfers' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'set_cases' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'set_intros' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'set_sels' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'set_thms' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'rel_cases' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'rel_intros' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'rel_sels' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'map_sels' to 'fp_sugar'
2014-10-06 desharna 2014-10-06 add 'map_disc_iffs' to 'fp_sugar'
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar move theorems
2014-09-26 desharna 2014-09-26 refactor fp_sugar with empty substructures
2014-09-15 blanchet 2014-09-15 tuning
2014-09-15 blanchet 2014-09-15 generate 'code' attribute only if 'code' plugin is enabled
2014-09-11 blanchet 2014-09-11 tuning terminology
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 proper checks -- the calls data structure may contain spurious entries
2014-09-09 blanchet 2014-09-09 more canonical (and correct) local theory threading
2014-09-08 blanchet 2014-09-08 made N2M work with sort constraints (cf. TODO)
2014-09-08 blanchet 2014-09-08 honour sorts in N2M
2014-09-08 blanchet 2014-09-08 improved caching
2014-09-08 blanchet 2014-09-08 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
2014-09-04 blanchet 2014-09-04 moved code around
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-01 blanchet 2014-09-01 drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'
2014-09-01 blanchet 2014-09-01 more compatibility between old- and new-style datatypes
2014-09-01 blanchet 2014-09-01 made transfer functions slightly more general
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-08-12 blanchet 2014-08-12 improved unfolding of 'let's
2014-08-12 blanchet 2014-08-12 less aggressive unfolding; removed debugging;
2014-07-02 desharna 2014-07-02 generate 'corec_code' theorem for codatatypes
2014-06-27 blanchet 2014-06-27 tuned variable names