src/HOL/Tools/Datatype/datatype_prop.ML
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2013-11-12 blanchet 2013-11-12 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
2012-11-26 wenzelm 2012-11-26 tuned signature; tuned;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2012-01-14 wenzelm 2012-01-14 renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_all_free in favour of plain Logic.all;
2011-12-16 wenzelm 2011-12-16 tuned signature;
2011-12-15 wenzelm 2011-12-15 misc tuning and simplification;
2011-12-14 wenzelm 2011-12-14 avoid fragile Sign.intern_const -- pass internal names directly; tuned;
2011-12-12 wenzelm 2011-12-12 datatype dtyp with explicit sort information; tuned messages;
2011-12-12 wenzelm 2011-12-12 tuned;
2011-12-02 wenzelm 2011-12-02 misc tuning;
2011-12-02 wenzelm 2011-12-02 tuned whitespace;
2011-12-02 wenzelm 2011-12-02 eliminated some legacy operations;
2011-11-30 wenzelm 2011-11-30 misc tuning;
2011-10-21 wenzelm 2011-10-21 tuned;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-04-08 wenzelm 2011-04-08 discontinued special treatment of structure Lexicon;
2010-12-30 wenzelm 2010-12-30 do not open auxiliary ML structures;
2010-12-01 wenzelm 2010-12-01 more direct use of binder_types/body_type;
2010-11-26 wenzelm 2010-11-26 explicit use of unprefix;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-02-25 wenzelm 2010-02-25 more antiquotations;
2010-02-23 bulwahn 2010-02-23 adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening
2009-11-30 haftmann 2009-11-30 modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
2009-11-25 haftmann 2009-11-25 normalized uncurry take/drop
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 Datatype.read_typ: standard argument order; eliminated some old folds;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-06-23 haftmann 2009-06-23 uniformly capitialized names for subdirectories