src/HOL/Tools/TFL/casesplit.ML
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-09-17 blanchet 2014-09-17 support (finite values of) codatatypes in Quickcheck
2014-09-01 blanchet 2014-09-01 ported TFL to mixture of old and new datatypes
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
2014-09-01 blanchet 2014-09-01 tuned structure inclusion
2014-02-01 wenzelm 2014-02-01 proper context for printing;
2013-05-30 wenzelm 2013-05-30 prefer existing beta_eta_conversion;
2012-09-12 wenzelm 2012-09-12 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
2012-02-15 wenzelm 2012-02-15 removed dead code;
2011-11-30 wenzelm 2011-11-30 discontinued obsolete datatype "alt_names";
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-04-16 wenzelm 2011-04-16 more direct Logic.dest_implies (with exception TERM instead of Subscript);
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
2011-02-25 krauss 2011-02-25 removed dead code/unused exports/speculative generality
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
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-09-28 haftmann 2009-09-28 avoid compound fields in datatype info record
2009-09-27 haftmann 2009-09-27 registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-06-23 haftmann 2009-06-23 tuned interfaces of datatype module
2009-06-19 haftmann 2009-06-19 discontinued ancient tradition to suffix certain ML module names with "_package"
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2007-05-31 wenzelm 2007-05-31 moved TFL files to canonical place;