src/HOL/Tools/BNF/bnf_gfp.ML
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
2014-03-04 blanchet 2014-03-04 renamed a pair of low-level theorems to have c/dtor in their names (like the others)
2014-03-04 traytel 2014-03-04 N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
2014-03-04 blanchet 2014-03-04 removed debugging leftover
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 optimize cardinal bounds involving natLeq (omega)
2014-02-25 traytel 2014-02-25 joint work with blanchet: intermediate typedef for the input to fp-operations
2014-02-26 traytel 2014-02-26 intermediate typedef for the type of the bound (local to lfp)
2014-02-26 traytel 2014-02-26 made tactics more robust
2014-02-21 traytel 2014-02-21 only one internal coinduction rule
2014-02-21 blanchet 2014-02-21 adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
2014-02-20 traytel 2014-02-20 made tactics more robust
2014-02-19 traytel 2014-02-19 another simplification of internal codatatype construction
2014-02-19 traytel 2014-02-19 simplifications of internal codatatype construction
2014-02-18 traytel 2014-02-18 syntactic simplifications of internal (co)datatype constructions
2014-02-17 blanchet 2014-02-17 tuning * * * moved 'primrec' up to displace the few remaining uses of 'old_primrec'
2014-02-17 blanchet 2014-02-17 tuning: moved code where it belongs
2014-02-14 traytel 2014-02-14 register bnfs for (co)datatypes under their proper name (lost in af71b753c459)
2014-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
2014-02-12 blanchet 2014-02-12 se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
2014-01-31 traytel 2014-01-31 use Local_Theory.define instead of Specification.definition for internal constants
2014-01-31 traytel 2014-01-31 less hermetic tactics
2014-01-20 blanchet 2014-01-20 tuned names
2014-01-20 blanchet 2014-01-20 made BNF compile after move to HOL
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories