src/HOL/Tools/BNF/bnf_def.ML
2015-03-16 traytel 2015-03-16 BNF relators preserve reflexivity
2015-03-10 blanchet 2015-03-10 split into subgoals
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-01-05 blanchet 2015-01-05 added plugins syntax to prim(co)rec
2014-12-11 traytel 2014-12-11 note more facts (always)
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-10-13 wenzelm 2014-10-13 clarified load order; tuned signature;
2014-10-13 wenzelm 2014-10-13 Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
2014-10-08 wenzelm 2014-10-08 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
2014-09-24 blanchet 2014-09-24 improved 'bnf' parser
2014-09-16 blanchet 2014-09-16 register 'prod' and 'sum' as datatypes, to allow N2M through them
2014-09-15 blanchet 2014-09-15 set 'mono' attribute on 'rel_mono'
2014-09-05 blanchet 2014-09-05 added 'plugins' option to control which hooks are enabled
2014-09-05 blanchet 2014-09-05 introduced mechanism to filter interpretations
2014-09-05 blanchet 2014-09-05 fixed infinite loops in 'register' functions + more uniform API
2014-09-05 blanchet 2014-09-05 named interpretations
2014-09-05 blanchet 2014-09-05 centralized and cleaned up naming handling
2014-09-03 blanchet 2014-09-03 introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-09-03 blanchet 2014-09-03 tuned BNF database handling
2014-09-01 blanchet 2014-09-01 added theory-based getters for convenience
2014-09-01 blanchet 2014-09-01 tuned whitespace
2014-09-01 desharna 2014-09-01 generate 'set_transfer' for BNFs
2014-09-01 desharna 2014-09-01 generate 'rel_transfer' for BNFs
2014-09-01 desharna 2014-09-01 note 'map_transfer' more often
2014-08-29 desharna 2014-08-29 generate 'case_transfer' for (co)datatypes
2014-08-18 desharna 2014-08-18 generate 'map_cong_simp' for BNFs
2014-08-18 desharna 2014-08-18 generate 'inj_map_strong' for BNFs
2014-08-18 desharna 2014-08-18 note 'inj_map' more often
2014-08-18 desharna 2014-08-18 generate property 'rel_mono_strong' for BNFs
2014-08-18 desharna 2014-08-18 renamed 'rel_mono_strong' to 'rel_mono_strong0'
2014-08-14 desharna 2014-08-14 generate 'rel_map' theorem for BNFs
2014-07-25 blanchet 2014-07-25 tuning
2014-07-24 blanchet 2014-07-24 use the noted theorems in 'BNF_Comp'
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-07-09 blanchet 2014-07-09 got rid of a pointer equality
2014-06-27 blanchet 2014-06-27 compile
2014-06-24 desharna 2014-06-24 tune the implementation of 'rel_coinduct'
2014-06-24 desharna 2014-06-24 generate 'rel_coinduct0' theorem for codatatypes
2014-05-08 desharna 2014-05-08 note map_id0 more often
2014-05-08 desharna 2014-05-08 generate 'map_ident' theorem for BNFs
2014-04-28 blanchet 2014-04-28 more reliable 'name_of_bnf'
2014-04-23 blanchet 2014-04-23 made SML/NJ happier
2014-04-23 blanchet 2014-04-23 localize new size function generation code
2014-04-23 blanchet 2014-04-23 added 'inj_map' as auxiliary BNF theorem
2014-04-10 kuncar 2014-04-10 revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
2014-04-10 kuncar 2014-04-10 don't forget to init Interpretation and transfer theorems in the interpretation hook
2014-04-03 blanchet 2014-04-03 added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
2014-04-01 blanchet 2014-04-01 added BNF interpretation hook
2014-03-10 traytel 2014-03-10 unfold intermediate definitions after sealing the bnf
2014-03-06 blanchet 2014-03-06 renamed 'fun_rel' to 'rel_fun'
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
2014-02-14 blanchet 2014-02-14 allow different functions to recurse on the same type, like in the old package
2014-02-12 blanchet 2014-02-12 iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
2014-02-12 blanchet 2014-02-12 more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's
2014-02-07 blanchet 2014-02-07 reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
2014-02-06 blanchet 2014-02-06 allow multiple registration of the same type, the last wins
2014-01-31 traytel 2014-01-31 less hermetic tactics