2010-03-27 ago added Term.fold_atyps_sorts convenience;
2010-02-19 ago added dest_comb
2010-01-28 ago tuned signature;
2009-11-15 ago tuned;
2009-11-09 ago locale_const/target_notation: uniform use of Term.aconv_untyped;
2009-10-22 ago map_range (and map_index) combinator
2009-09-30 ago eliminated redundant bindings;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-26 ago lambda/cabs/all: named variants;
2009-07-16 ago use structure Same;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 ago close_schematic_term: uniform order of types/terms;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-02-27 ago eliminated NJ's List.nth;
2009-02-27 ago tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
2009-02-13 ago New command find_consts searching for constants by type (by Timothy Bourke).
2009-01-01 ago added canonical add_const_names, add_consts;
2008-12-31 ago updated header;
2008-12-31 ago added declare_term_frees;
2008-12-31 ago moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-12-31 ago moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-30 ago provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names;
2008-12-30 ago removed unused head_name_of;
2008-06-23 ago moved implies to logic.ML;
2007-10-16 ago tuned hidden_polymorphism;
2007-10-11 ago replaced Term.equiv_types by Type.similar_types;
2007-10-04 ago Name.uu, Name.aT;
2007-09-29 ago added declare_typ_names;
2007-09-26 ago added free_dummy_patterns;
2007-09-21 ago added has_abs (from envir.ML);
2007-08-30 ago added burrow_types;
2007-05-31 ago simplified/unified list fold;
2007-05-10 ago tuned argument_type_of;
2007-04-17 ago export is_dummy_pattern;
2007-04-12 ago absdummy: use internal name uu to avoid renaming of popular names;
2007-04-03 ago signature: eqtype to accomodate Alice;
2007-01-09 ago added map_abs_vars
2007-01-02 ago Term.lambda: abstract over arbitrary closed terms;
2006-12-12 ago added equiv_types;
2006-12-10 ago tuned absdummy;
2006-12-06 ago added hidden_polymorphism (from variable.ML);
2006-11-23 ago added head_name_of;
2006-11-14 ago added dummyS;
2006-10-13 ago fixed bug
2006-10-04 ago insert replacing ins ins_int ins_string
2006-09-21 ago member (op =);
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-13 ago added exists_type;
2006-09-12 ago removed obsolete aconvs (use eq_list aconv);
2006-08-03 ago removed obsolete add_term_tvarnames;
2006-07-27 ago declare_term_names: cover types as well;
2006-07-25 ago is_funtype: do not export internal operation;
2006-07-19 ago added variant_frees;
2006-07-18 ago added declare_term_names;
2006-07-14 ago Term.term_lpo takes order on terms rather than strings as argument.
2006-07-13 ago strip_abs_eta: proper use of Name.context;
2006-07-12 ago removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);