2014-04-03 blanchet 2014-04-03 added same idiomatic handling of namings for Ctr_Sugar/BNF-related interpretation hooks as for typedef and (old-style) datatypes
2014-04-01 blanchet 2014-04-01 added 'ctr_sugar' interpretation hook
2014-02-17 blanchet 2014-02-17 name derivations in 'primrec' for code extraction from proof terms
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 removed needless robustness (no longer needed thanks to new syntax)
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 have 'Ctr_Sugar' register its 'Spec_Rules'
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 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 use right local theory -- shows up when 'no_discs_sels' is set
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-10 blanchet 2014-01-10 only destruct cases equipped with the right stuff (in particular, 'sel_split')
2014-01-02 blanchet 2014-01-02 generate 'disc_iff' property in 'primcorec'
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-12-09 blanchet 2013-12-09 tuning -- moved ML files to subdirectory