src/HOL/Tools/TFL/tfl.ML
2010-05-05 ago farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-05-03 ago replaced Thm.legacy_freezeT by Thm.unvarify_global -- these facts stem from closed definitions, i.e. there are no term Vars;
2010-05-03 ago renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-03-15 ago preserve full const name more carefully, and avoid slightly odd Sign.intern_term;
2010-03-09 ago renamed mk_const_def to legacy_const_def, because of slightly odd Sign.intern_term;
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-11-24 ago curried take/drop
2009-10-29 ago eliminated some old folds;
2009-10-29 ago standardized filter/filter_out;
2009-10-22 ago map_range (and map_index) combinator
2009-10-21 ago merged
2009-10-21 ago curried union as canonical list operation
2009-10-21 ago removed old-style \ and \\ infixes
2009-10-21 ago merged
2009-10-21 ago dropped redundant gen_ prefix
2009-10-21 ago standardized basic operations on type option;
2009-10-15 ago replaced String.concat by implode;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-28 ago modernized messages -- eliminated ctyp/cterm operations;
2009-07-21 ago proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-06-23 ago tuned interfaces of datatype module
2009-06-19 ago discontinued ancient tradition to suffix certain ML module names with "_package"
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-01 ago use long names for old-style fold combinators;
2009-01-21 ago binding replaces bstring
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-05-17 ago structure Display: less pervasive operations;
2008-02-28 ago removed legacy ML bindings;
2007-08-30 ago replaced ProofContext.infer_types by general Syntax.check_terms;
2007-05-31 ago moved TFL files to canonical place;