src/HOL/Tools/BNF/bnf_def.ML
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-10-01 blanchet 2015-10-01 export '_cmd' functions
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-24 traytel 2015-09-24 conceal only the definitional theorems of map, set, rel (and not the actual constants)
2015-09-24 traytel 2015-09-24 more useful properties of the relators
2015-09-04 wenzelm 2015-09-04 close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
2015-09-03 traytel 2015-09-03 use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
2015-08-16 wenzelm 2015-08-16 prefer theory_id operations; tuned signature;
2015-08-13 wenzelm 2015-08-13 merged
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2015-08-12 traytel 2015-08-12 new command for lifting BNF structure over typedefs
2015-07-27 wenzelm 2015-07-27 tuned signature;
2015-07-26 wenzelm 2015-07-26 updated to infer_instantiate;
2015-07-17 traytel 2015-07-17 forgotten selector
2015-07-16 traytel 2015-07-16 {r,e,d,f}tac with proper context in BNF
2015-04-28 blanchet 2015-04-28 allow sorts on dead variables in BNFs
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
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-27 blanchet 2015-03-27 sort BNFs in output
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