src/HOL/Tools/BNF/bnf_fp_util.ML
16 months ago wenzelm 2017-11-26 more symbols;
2016-10-26 blanchet 2016-10-26 tuning
2016-09-12 blanchet 2016-09-12 prove 'set' property backward
2016-09-11 blanchet 2016-09-11 provide a mechanism for ensuring dead type variables occur in typedef if desired
2016-09-08 blanchet 2016-09-08 made it easier to catch 'empty datatype' exception
2016-09-07 blanchet 2016-09-07 tuned whitespace
2016-09-06 blanchet 2016-09-06 generalized ML signature
2016-09-06 blanchet 2016-09-06 generalized code (subtly)
2016-09-06 blanchet 2016-09-06 tuned ML signature
2016-09-05 blanchet 2016-09-05 export ML function + tuning
2016-04-14 traytel 2016-04-14 n2m operates on (un)folds
2016-04-07 traytel 2016-04-07 (un)folds are not legacy
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 generalized ML function
2016-03-28 blanchet 2016-03-28 added '_legacy' suffixes
2016-03-28 blanchet 2016-03-28 generalized ML interface
2016-03-22 blanchet 2016-03-22 added timers to N2M
2016-03-22 traytel 2016-03-22 document that n2m does not depend on most things in fp_sugar in its type
2016-03-14 blanchet 2016-03-14 generalized ML function
2016-02-17 blanchet 2016-02-17 making 'pred_inject' a first-class BNF citizen
2016-01-11 blanchet 2016-01-11 tuning
2016-01-11 blanchet 2016-01-11 exported ML function
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-16 blanchet 2015-07-16 tuning
2015-07-05 wenzelm 2015-07-05 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 blanchet 2015-04-01 simplified code
2015-03-31 wenzelm 2015-03-31 merged
2015-03-31 wenzelm 2015-03-31 tuned signature;
2015-03-30 wenzelm 2015-03-30 support for strictly private name space entries; 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-10 blanchet 2015-03-10 tuning
2015-03-06 wenzelm 2015-03-06 clarified context;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-03-03 traytel 2015-03-03 eliminated some clones of Proof_Context.cterm_of
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
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-25 desharna 2014-09-25 generate 'ctor_rec_transfer' for datatypes
2014-09-01 traytel 2014-09-01 goal generation for xtor_co_rec_transfer
2014-09-25 traytel 2014-09-25 even more deads go to the end (continuation of e3a01b73579f)
2014-09-13 blanchet 2014-09-13 imported patch phantoms
2014-09-09 blanchet 2014-09-09 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 blanchet 2014-09-09 generalized 'datatype' LaTeX antiquotation and added 'codatatype'
2014-09-08 blanchet 2014-09-08 tuning
2014-09-04 blanchet 2014-09-04 moved code around
2014-09-03 blanchet 2014-09-03 tuning