formal position for PThm nodes;

isabelle update -u control_cartouches;

made tactics more robust

store the unfolded definitions of the lifted bnf constants under "_def" name

more error checking

generalized ML function (towards nonuniform datatypes)

tuned signature

union associates to the left

prove 'set' property backward

derive pred_mono property for BNFs

more antiquotations;

tuned proofs, to allow unfold_abs_def;

tuned;

generalized ML function

generalized ML function

derive transfer rule for predicator

allow predicator instead of map function in 'primrec'

make predicator a first-class bnf citizen

more uniform treatment of package internals;

more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;

tuned whitespace

prod_case as canonical name for product type eliminator

collect the names from goals in favor of fragile exports

export '_cmd' functions

more canonical context threading

congruence rules for the relator

conceal only the definitional theorems of map, set, rel (and not the actual constants)

more useful properties of the relators

close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;

use open/close_target rather than Local_Theory.restore to get polymorphic definitions;

prefer theory_id operations;
tuned signature;

tuned signature, in accordance to sortBy in Scala;

new command for lifting BNF structure over typedefs

tuned signature;

updated to infer_instantiate;

forgotten selector

{r,e,d,f}tac with proper context in BNF

allow sorts on dead variables in BNFs

@{command_spec} is superseded by @{command_keyword};

tuned signature;

support for strictly private name space entries;
tuned signature;

sort BNFs in output

BNF relators preserve reflexivity

split into subgoals

Thm.cterm_of and Thm.ctyp_of operate on local context;

eliminated some clones of Proof_Context.cterm_of

added plugins syntax to prim(co)rec

note more facts (always)

renamed "pairself" to "apply2", in accordance to @{apply 2};

allow sorts on dead variables in BNFs

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

clarified load order;
tuned signature;

Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;

added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};

improved 'bnf' parser

register 'prod' and 'sum' as datatypes, to allow N2M through them

set 'mono' attribute on 'rel_mono'

added 'plugins' option to control which hooks are enabled

introduced mechanism to filter interpretations

fixed infinite loops in 'register' functions + more uniform API

named interpretations

centralized and cleaned up naming handling

introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales

tuned BNF database handling

added theory-based getters for convenience

tuned whitespace

generate 'set_transfer' for BNFs

generate 'rel_transfer' for BNFs

note 'map_transfer' more often

generate 'case_transfer' for (co)datatypes

generate 'map_cong_simp' for BNFs

generate 'inj_map_strong' for BNFs

note 'inj_map' more often

generate property 'rel_mono_strong' for BNFs

renamed 'rel_mono_strong' to 'rel_mono_strong0'

generate 'rel_map' theorem for BNFs

tuning

use the noted theorems in 'BNF_Comp'

use the noted theorem whenever possible, also in 'BNF_Def'

add mk_Trueprop_mem utility function

got rid of a pointer equality

compile

tune the implementation of 'rel_coinduct'

generate 'rel_coinduct0' theorem for codatatypes

note map_id0 more often

generate 'map_ident' theorem for BNFs

more reliable 'name_of_bnf'

made SML/NJ happier

localize new size function generation code

added 'inj_map' as auxiliary BNF theorem

revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created

don't forget to init Interpretation and transfer theorems in the interpretation hook

added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes

added BNF interpretation hook

unfold intermediate definitions after sealing the bnf

renamed 'fun_rel' to 'rel_fun'

make 'typedef' optional, depending on size of original type

allow different functions to recurse on the same type, like in the old package

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')

more liberal merging of BNFs and constructor sugar
* * *
make sure that the cache doesn't produce 'DUP's

reverted a87e49f4336d -- overwriting of data entries yields to merge problems later

allow multiple registration of the same type, the last wins

less hermetic tactics

adjusted comments

avoid nested 'Tools' directories

--HG--
rename : src/HOL/Tools/BNF/Tools/bnf_comp.ML => src/HOL/Tools/BNF/bnf_comp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_comp_tactics.ML => src/HOL/Tools/BNF/bnf_comp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def.ML => src/HOL/Tools/BNF/bnf_def.ML
rename : src/HOL/Tools/BNF/Tools/bnf_def_tactics.ML => src/HOL/Tools/BNF/bnf_def_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_def_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m.ML => src/HOL/Tools/BNF/bnf_fp_n2m.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_sugar.ML => src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_n2m_tactics.ML => src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_rec_sugar_util.ML => src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_fp_util.ML => src/HOL/Tools/BNF/bnf_fp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp.ML => src/HOL/Tools/BNF/bnf_gfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_tactics.ML => src/HOL/Tools/BNF/bnf_gfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_gfp_util.ML => src/HOL/Tools/BNF/bnf_gfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp.ML => src/HOL/Tools/BNF/bnf_lfp.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_compat.ML => src/HOL/Tools/BNF/bnf_lfp_compat.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_rec_sugar.ML => src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_tactics.ML => src/HOL/Tools/BNF/bnf_lfp_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_lfp_util.ML => src/HOL/Tools/BNF/bnf_lfp_util.ML
rename : src/HOL/Tools/BNF/Tools/bnf_tactics.ML => src/HOL/Tools/BNF/bnf_tactics.ML
rename : src/HOL/Tools/BNF/Tools/bnf_util.ML => src/HOL/Tools/BNF/bnf_util.ML