src/HOL/Tools/BNF/bnf_fp_util.ML
2016-04-03 ago tuned names
2016-03-28 ago generalized ML function
2016-03-28 ago added '_legacy' suffixes
2016-03-28 ago generalized ML interface
2016-03-22 ago added timers to N2M
2016-03-22 ago document that n2m does not depend on most things in fp_sugar in its type
2016-03-14 ago generalized ML function
2016-02-17 ago making 'pred_inject' a first-class BNF citizen
2016-01-11 ago tuning
2016-01-11 ago exported ML function
2016-01-07 ago more uniform treatment of package internals;
2015-07-27 ago tuned signature;
2015-07-16 ago tuning
2015-07-05 ago simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-04-01 ago simplified code
2015-03-31 ago merged
2015-03-31 ago tuned signature;
2015-03-30 ago support for strictly private name space entries;
2015-03-30 ago export more low-level theorems in data structure (partly for 'corec')
2015-03-26 ago store low-level (un)fold constants
2015-03-10 ago tuning
2015-03-06 ago clarified context;
2015-03-06 ago Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 ago tuned signature -- prefer qualified names;
2015-03-03 ago eliminated some clones of Proof_Context.cterm_of
2014-11-26 ago renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-08 ago added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-10-06 ago rename 'xtor_rel_thms' to 'xtor_rels'
2014-10-06 ago rename 'xtor_set_thmss' to 'xtor_setss'
2014-10-06 ago rename 'xtor_map_thms' to 'xtor_maps'
2014-10-06 ago rename 'xtor_co_rec_transfer_thms' to 'xtor_co_rec_transfers'
2014-10-06 ago rename 'dtor_set_induct_thms' to 'dtor_set_inducts'
2014-10-06 ago rename 'rel_xtor_co_induct_thm' to 'xtor_rel_co_induct'
2014-10-06 ago rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
2014-09-25 ago generate 'corec_transfer' for codatatypes
2014-09-25 ago generate 'rec_transfer' for datatypes
2014-09-25 ago generate 'dtor_corec_transfer' for codatatypes
2014-09-25 ago generate 'ctor_rec_transfer' for datatypes
2014-09-01 ago goal generation for xtor_co_rec_transfer
2014-09-25 ago even more deads go to the end (continuation of e3a01b73579f)
2014-09-13 ago imported patch phantoms
2014-09-09 ago nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
2014-09-09 ago generalized 'datatype' LaTeX antiquotation and added 'codatatype'
2014-09-08 ago tuning
2014-09-04 ago moved code around
2014-09-03 ago tuning
2014-09-01 ago more compatibility between old- and new-style datatypes
2014-09-01 ago made transfer functions slightly more general
2014-08-18 ago reordered some (co)datatype property names for more consistency
2014-07-30 ago generate 'set_induct' theorem for codatatypes
2014-07-25 ago tuning
2014-07-16 ago generate 'rel_sel' theorem for (co)datatypes
2014-07-07 ago refactor some tactics
2014-07-07 ago generate 'rel_cases' theorem for (co)datatypes
2014-07-03 ago generate 'rel_intros' theorem for (co)datatypes
2014-07-02 ago generate 'corec_code' theorem for codatatypes
2014-06-27 ago tuned variable names
2014-04-23 ago no need to make 'size' generation an interpretation -- overkill
2014-03-13 ago simplified internal codatatype construction
2014-03-07 ago more antiquotations;