isabelle update -u control_cartouches;

export ML functions (towards nonuniform codatatypes) + signature tuning

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

generalized ML signature

tuned ML signature

honor sorts in (co)datatype declarations

reintroduced check that may guard some tactic failures

generalized ML function

generalized ML interface

tuning

more general, reliable N2M

added timers to N2M

document that n2m does not depend on most things in fp_sugar in its type

making 'pred_inject' a first-class BNF citizen

allow predicator instead of map function in 'primrec'

keep 'ctor_iff_dtor' theorem around in BNF FP database

don't pollute local theory with needless names

prod_case as canonical name for product type eliminator

collect the names from goals in favor of fragile exports

prefer "uncurry" as canonical name for case distinction on products in combinatorial view

tuning

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

improved message in 'co' case

proper Envir.norm_type for result of Type.raw_unifys;

generate 'map_o_corec' for (co)datatypes
* * *
document 'map_o_corec'

move theorem 'rec_o_map'
* * *
move documentation of 'rec_o_map'

generate 'sel_transfer' for (co)datatypes

add 'fp_bnf' to 'bnf_sugar'

preserve the structure of 'set_intros' theorem in ML

preserve the structure of 'map_sel' theorem in ML

preserve the structure of 'set_sel' theorem in ML

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

add 'set_inducts' to 'fp_sugar'

add 'common_set_inducts' to 'fp_sugar'

add 'rel_co_inducts' to 'fp_sugar'

add 'common_rel_co_induct' to 'fp_sugar'

add 'co_rec_transfers' to 'fp_sugar'

add 'co_rec_disc_iffs' to 'fp_sugar'

add 'disc_transfers' to 'fp_sugar'

add 'case_transfers' to 'fp_sugar'

add 'ctr_transfers' to 'fp_sugar'

add 'set_cases' to 'fp_sugar'

add 'set_intros' to 'fp_sugar'

add 'set_sels' to 'fp_sugar'

add 'set_thms' to 'fp_sugar'

add 'rel_cases' to 'fp_sugar'

add 'rel_intros' to 'fp_sugar'

add 'rel_sels' to 'fp_sugar'

add 'map_sels' to 'fp_sugar'

add 'map_disc_iffs' to 'fp_sugar'

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar move theorems

refactor fp_sugar with empty substructures

tuning

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

tuning terminology

updated news

proper checks -- the calls data structure may contain spurious entries

more canonical (and correct) local theory threading

made N2M work with sort constraints (cf. TODO)

honour sorts in N2M

improved caching

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

moved code around

tuned size function generation

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

more compatibility between old- and new-style datatypes

made transfer functions slightly more general

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

improved unfolding of 'let's

less aggressive unfolding; removed debugging;

generate 'corec_code' theorem for codatatypes

tuned variable names

no need to make 'size' generation an interpretation -- overkill

manual merge + added 'rel_distincts' field to record for symmetry

reverted rb458558cbcc2 -- better to keep 'case' and 'rec' distinct, otherwise we lose the connection between 'ctor_rec' (the low-level recursor) and 'rec'

generate size instances for new-style datatypes

generate cliques for 'prim(co)rec' N2M

thread mutual cliques through

export theorems

balance tuples that represent curried functions

rationalized internals

rationalized internals

rationalized internals

rationalize internals

optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant

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

joint work with blanchet: intermediate typedef for the input to fp-operations

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

improved accounting for dead variables when naming set functions (refines d71c2737ee21)

added explicit killing

moved 'primrec' up (for real this time) and removed temporary 'old_primrec'

tuning

simplified data structure by reducing the incidence of clumsy indices

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

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

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

renamed '{prod,sum,bool,unit}_case' to 'case_...'

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

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

expand 'split' in direct corecursion as well

fixed handling of 'split'

made SML/NJ happier

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