src/HOL/Tools/BNF/bnf_gfp.ML
2016-04-07 traytel 2016-04-07 derive (co)rec uniformly from (un)fold
2016-04-05 traytel 2016-04-05 single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
2016-04-03 traytel 2016-04-03 tuned names
2016-03-28 blanchet 2016-03-28 added '_legacy' suffixes
2016-03-22 traytel 2016-03-22 document that n2m does not depend on most things in fp_sugar in its type
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
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-25 traytel 2015-09-25 restructure fresh variable generation to make exports more wellformed
2015-09-25 traytel 2015-09-25 more canonical context threading
2015-09-24 traytel 2015-09-24 congruence rules for the relator
2015-09-03 traytel 2015-09-03 use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate;
2015-07-16 traytel 2015-07-16 {r,e,d,f}tac with proper context in BNF
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-31 wenzelm 2015-03-31 merged
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-30 blanchet 2015-03-30 export more low-level theorems in data structure (partly for 'corec')
2015-03-26 blanchet 2015-03-26 store low-level (un)fold constants
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper proof context for typedef;
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 rename 'xtor_rel_thms' to 'xtor_rels'
2014-10-06 desharna 2014-10-06 rename 'xtor_set_thmss' to 'xtor_setss'
2014-10-06 desharna 2014-10-06 rename 'xtor_map_thms' to 'xtor_maps'
2014-10-06 desharna 2014-10-06 rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
2014-10-06 desharna 2014-10-06 rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
2014-10-06 desharna 2014-10-06 rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
2014-10-06 desharna 2014-10-06 rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
2014-09-25 desharna 2014-09-25 generate 'corec_transfer' for codatatypes
2014-09-25 desharna 2014-09-25 generate 'rec_transfer' for datatypes
2014-09-25 desharna 2014-09-25 generate 'dtor_corec_transfer' for codatatypes
2014-09-01 traytel 2014-09-01 goal generation for xtor_co_rec_transfer
2014-09-09 blanchet 2014-09-09 generalized 'datatype' LaTeX antiquotation and added 'codatatype'
2014-09-08 blanchet 2014-09-08 generate better internal names, with name of the target type in it
2014-09-08 blanchet 2014-09-08 tuning
2014-09-04 blanchet 2014-09-04 tuned size function generation
2014-09-03 blanchet 2014-09-03 introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-08-19 blanchet 2014-08-19 don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
2014-08-14 desharna 2014-08-14 generate 'rel_map' theorem for BNFs
2014-07-31 traytel 2014-07-31 simplified tactics slightly
2014-07-30 desharna 2014-07-30 generate 'set_induct' theorem for codatatypes
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-17 desharna 2014-07-17 add mk_Trueprop_mem utility function
2014-05-26 blanchet 2014-05-26 don't conceal (co)datatypes
2014-04-28 blanchet 2014-04-28 more reliable 'name_of_bnf'
2014-04-10 traytel 2014-04-10 more accurate type arguments for intermeadiate typedefs
2014-04-01 blanchet 2014-04-01 tuning
2014-04-01 blanchet 2014-04-01 added BNF interpretation hook
2014-03-25 traytel 2014-03-25 prove theorems with fixed variables (export afterwards)
2014-03-17 traytel 2014-03-17 tuned internal construction
2014-03-13 traytel 2014-03-13 tuned tactics
2014-03-13 traytel 2014-03-13 simplified internal codatatype construction
2014-03-10 traytel 2014-03-10 tuned tactic
2014-03-10 traytel 2014-03-10 unfold intermediate definitions after sealing the bnf