2014-08-18 blanchet 2014-08-18 reordered some (co)datatype property names for more consistency
2014-08-10 wenzelm 2014-08-10 merged -- with manual conflict resolution for src/HOL/SMT_Examples/SMT_Examples.certs2, src/HOL/SMT_Examples/SMT_Word_Examples.certs2, src/Doc/Prog_Prove/document/intro-isabelle.tex;
2014-07-30 blanchet 2014-07-30 correctly resolve selector names in default value equations
2014-07-30 desharna 2014-07-30 generate 'set_induct' theorem for codatatypes
2014-07-24 blanchet 2014-07-24 repaired named derivations
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, also in 'BNF_Def'
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
2014-06-16 blanchet 2014-06-16 fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
2014-06-10 blanchet 2014-06-10 use 'where' clause for selector default value syntax
2014-05-27 blanchet 2014-05-27 don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
2014-05-26 blanchet 2014-05-26 got rid of '=:' squiggly
2014-05-26 blanchet 2014-05-26 use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
2014-05-21 blanchet 2014-05-21 move exhaust first, for technical reasons
2014-05-05 blanchet 2014-05-05 simplify selectors in code views
2014-04-28 blanchet 2014-04-28 restored naming trick
2014-04-23 blanchet 2014-04-23 made SML/NJ happier
2014-04-10 kuncar 2014-04-10 revert idiomatic handling of namings from 5a93b8f928a2 because in combination with Named_Target.theory_init global names are sometimes created
2014-04-10 kuncar 2014-04-10 don't forget to init Interpretation and transfer theorems in the interpretation hook
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