src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
2014-02-17 blanchet 2014-02-17 name derivations in 'primrec' for code extraction from proof terms
2014-02-14 blanchet 2014-02-14 generate proper 'DtRec' indices in 'datatype_new_compat' for the case where some types are duplicated
2014-02-14 blanchet 2014-02-14 tuned code to allow mutualized corecursion through different functions with the same target type
2014-02-14 blanchet 2014-02-14 allow different functions to recurse on the same type, like in the old package
2014-02-14 blanchet 2014-02-14 more precise spec rules for selectors
2014-02-14 blanchet 2014-02-14 aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
2014-02-14 blanchet 2014-02-14 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
2014-02-14 blanchet 2014-02-14 register 'Spec_Rules' for new-style (co)datatypes
2014-02-12 blanchet 2014-02-12 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')
2014-02-12 blanchet 2014-02-12 renamed '{prod,sum,bool,unit}_case' to 'case_...'
2014-02-12 blanchet 2014-02-12 killed 'rep_compat' option
2014-02-12 blanchet 2014-02-12 made 'ctr_sugar' more friendly to the 'datatype_realizer' * * * reverted changes to 'datatype_realizer.ML'
2014-02-12 blanchet 2014-02-12 generate 'fundec_cong' attribute for new-style (co)datatypes * * * compile
2014-02-12 blanchet 2014-02-12 more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's
2014-02-07 blanchet 2014-02-07 reverted a87e49f4336d -- overwriting of data entries yields to merge problems later
2014-02-06 blanchet 2014-02-06 allow multiple registration of the same type, the last wins
2014-02-06 blanchet 2014-02-06 tuning
2014-01-21 blanchet 2014-01-21 made SML/NJ happier
2014-01-21 blanchet 2014-01-21 made SML/NJ happier
2014-01-20 blanchet 2014-01-20 removed dependency of BNF package on Nitpick
2014-01-20 blanchet 2014-01-20 adjusted comments
2014-01-20 blanchet 2014-01-20 avoid nested 'Tools' directories