formal position for PThm nodes;

isabelle update -u control_cartouches;

proper concept of code declaration wrt. atomicity and Isar declarations

--HG--
extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472

more uniform errors in '(prim)(co)rec(ursive)' variants

print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'

make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions

more robustness

tuned signature

explicit tagging of code equations de-baroquifies interface

--HG--
extra : rebase_source : 1d83d31f669dc30b586df508a64fdc3a9e7b2655

support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;

generalize code to avoid making assumptions about type variable names

respect qualification when noting theorems in prim(co)rec

make predicator a first-class bnf citizen

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

have 'primrec' return definitions

renamed ML funs

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

tuned;

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

tuned whitespace

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};

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar move theorems

tweaked compatibility layer

support (finite values of) codatatypes in Quickcheck

tuning

generate 'code' attribute only if 'code' plugin is enabled

tuning terminology

speed up old Nominal by killing type variables

made SML/NJ happier

export right sorts

wildcards in plugins

improved 'datatype_compat' further for recursion through functions

no type-based lookup -- these fail in the general, ambiguous case

tuning

properly note theorems for split recursors

tuning

extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions

added 'plugins' option to control which hooks are enabled

named interpretations

tuned size function generation

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

more compatibility functions

codatatypes are not datatypes

made SML/NJ happier

avoid more 'bad background theory' issues

drop hopeless feature -- unfolding of BNF datatype info without a prior 'datatype_compat'

ported to use new-style datatypes
* * *
compile

ported Refute to use new datatypes when possible

added primrec compatibility function

more work on compatibility interfaces

implemented compatibility definition of datatype

implemented compatibility interpretation

tuning

more compatibility between old- and new-style datatypes

tuning

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

--HG--
rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy
rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML
rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML
rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML
rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML
rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML
rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML

reordered some (co)datatype property names for more consistency

tuning

more correct clique computation for N2M

tuning whitespace

repaired named derivations

thread mutual cliques through

allow arguments to 'datatype_compat' in disorder

support deeply nested datatypes in 'datatype_compat'

preserve user type variable names to avoid mismatches/confusion

tuned signature;

balance tuples that represent curried functions

tuned signature -- more uniform check_type_name/read_type_name;
proper reports for read_type_name (lost in 710bc66f432c);

rationalize internals

got rid of automatically generated fold constant and theorems (to reduce overhead)

correct most general type for mutual recursion when several identical types are involved

prepare two-stage 'primrec' setup

tuning

follow up of 0819931d652d -- put right induction rule in the old data structure, repairs 'HOL-Proof'-based sessions

simplified data structure by reducing the incidence of clumsy indices

renamed 'datatype_new_compat' to 'datatype_compat'

generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated

better handling of recursion through functions

generate unique names

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

improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor

made 'ctr_sugar' more friendly to the 'datatype_realizer'
* * *
reverted changes to 'datatype_realizer.ML'

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