src/HOL/Tools/BNF/bnf_def.ML
18 months ago traytel 2017-12-17 made tactics more robust
23 months ago traytel 2017-07-11 store the unfolded definitions of the lifted bnf constants under "_def" name
24 months ago blanchet 2017-06-27 more error checking
2016-12-21 blanchet 2016-12-21 generalized ML function (towards nonuniform datatypes)
2016-11-01 traytel 2016-11-01 tuned signature
2016-09-13 blanchet 2016-09-13 union associates to the left
2016-09-12 blanchet 2016-09-12 prove 'set' property backward
2016-08-18 traytel 2016-08-18 derive pred_mono property for BNFs
2016-07-05 wenzelm 2016-07-05 more antiquotations;
2016-05-27 wenzelm 2016-05-27 tuned proofs, to allow unfold_abs_def;
2016-04-18 wenzelm 2016-04-18 tuned;
2016-03-01 blanchet 2016-03-01 generalized ML function
2016-02-26 blanchet 2016-02-26 generalized ML function
2016-02-17 traytel 2016-02-17 derive transfer rule for predicator
2016-02-17 blanchet 2016-02-17 allow predicator instead of map function in 'primrec'
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2016-01-07 wenzelm 2016-01-07 more uniform treatment of package internals;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-12-01 blanchet 2015-12-01 tuned whitespace
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