src/HOL/Ctr_Sugar.thy
2014-09-05 blanchet 2014-09-05 introduced mechanism to filter interpretations
2014-09-03 blanchet 2014-09-03 introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales
2014-07-24 blanchet 2014-07-24 use the noted theorem whenever possible, also in 'BNF_Def'
2014-03-07 wenzelm 2014-03-07 modernized theory setup;
2014-02-14 blanchet 2014-02-14 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
2014-01-29 blanchet 2014-01-29 added Dmitriy, since he did the case syntax
2013-12-09 blanchet 2013-12-09 tuning -- moved ML files to subdirectory
2013-12-02 blanchet 2013-12-02 added 'no_code' option
2013-12-02 blanchet 2013-12-02 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
2013-11-12 blanchet 2013-11-12 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
2013-11-12 blanchet 2013-11-12 tuned headers
2013-11-12 blanchet 2013-11-12 moved 'Ctr_Sugar' files out of BNF, so that it can become a general-purpose abstraction