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);
2006-07-12 ago added strip_abs_eta
2006-07-11 ago removed obsolete xless;
2006-07-11 ago removed obsolete ins_ix, mem_ix, ins_term, mem_term;
2006-07-04 ago added generalize/instantiate_option;
2006-06-17 ago added exists_subtype;
2006-05-16 ago removed low-level str_of_sort/typ/term (use Display.raw_string_of_sort/typ/term instead, or even PolyML.print -- for debugging purposes);
2006-04-26 ago tuned;
2006-04-24 ago cleaned up some diagnostic mathom
2006-04-10 ago added aT (from axclass.ML);
2006-02-16 ago tuned subst_bound(s);
2006-02-11 ago added variant_name;
2006-02-10 ago removed obsolete add_typ/term_classes/tycons;
2006-02-08 ago map_type_tvar/tfree: map_atyps;
2006-02-08 ago fixed the most silly bug conceivable in map_atyps
2006-02-07 ago lambda: base name of Const;
2006-02-06 ago lambda: abstract over any const;
2006-02-06 ago added strip_abs
2006-02-02 ago moved specific map_typ/term to sign.ML;
2006-01-31 ago lambda: abstract over TYPE argument, too;
2006-01-30 ago added map_atype, map_aterms
2005-11-25 ago added dummy_pattern;
2005-11-16 ago added betapplys;
2005-11-10 ago added find_free (from Isar/proof_context.ML);
2005-11-09 ago removed obsolete term set operations;
2005-10-15 ago tuned comments;
2005-10-07 ago added absdummy;
2005-10-07 ago added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-25 ago zero_var_inst: replace loose bounds :000 etc.;
2005-09-08 ago introduces some modern-style AList operations
2005-09-06 ago introduced some new-style AList operations
2005-08-01 ago removed atless (use term_ord instead);
2005-07-28 ago added add_tfreesT, add_tfrees;