src/Pure/term.ML
2007-10-04 wenzelm 2007-10-04 Name.uu, Name.aT;
2007-09-29 wenzelm 2007-09-29 added declare_typ_names; replace_dummy_patterns: canonical argument order;
2007-09-26 wenzelm 2007-09-26 added free_dummy_patterns;
2007-09-21 wenzelm 2007-09-21 added has_abs (from envir.ML);
2007-08-30 wenzelm 2007-08-30 added burrow_types;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-10 wenzelm 2007-05-10 tuned argument_type_of;
2007-04-17 wenzelm 2007-04-17 export is_dummy_pattern;
2007-04-12 wenzelm 2007-04-12 absdummy: use internal name uu to avoid renaming of popular names;
2007-04-03 wenzelm 2007-04-03 signature: eqtype to accomodate Alice;
2007-01-09 haftmann 2007-01-09 added map_abs_vars
2007-01-02 wenzelm 2007-01-02 Term.lambda: abstract over arbitrary closed terms;
2006-12-12 wenzelm 2006-12-12 added equiv_types;
2006-12-10 wenzelm 2006-12-10 tuned absdummy;
2006-12-06 wenzelm 2006-12-06 added hidden_polymorphism (from variable.ML);
2006-11-23 wenzelm 2006-11-23 added head_name_of;
2006-11-14 wenzelm 2006-11-14 added dummyS;
2006-10-13 haftmann 2006-10-13 fixed bug
2006-10-04 haftmann 2006-10-04 insert replacing ins ins_int ins_string
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-13 wenzelm 2006-09-13 added exists_type;
2006-09-12 wenzelm 2006-09-12 removed obsolete aconvs (use eq_list aconv); tuned aconv --- more efficient on identical subterms; moved term subst functions to term_subst.ML;
2006-08-03 wenzelm 2006-08-03 removed obsolete add_term_tvarnames;
2006-07-27 wenzelm 2006-07-27 declare_term_names: cover types as well; removed unused zero_var_indexesT; tuned;
2006-07-25 wenzelm 2006-07-25 is_funtype: do not export internal operation; added add_varnames (cf. add_vars etc.); removed obsolete (add_)term_varnames; removed find_free (moved to Isar/obtain.ML); moved variant_abs to structure Syntax -- this is a syntax operation after all;
2006-07-19 wenzelm 2006-07-19 added variant_frees; tuned;
2006-07-18 wenzelm 2006-07-18 added declare_term_names; tuned;
2006-07-14 ballarin 2006-07-14 Term.term_lpo takes order on terms rather than strings as argument.
2006-07-13 wenzelm 2006-07-13 strip_abs_eta: proper use of Name.context;
2006-07-12 wenzelm 2006-07-12 removed obsolete adhoc_freeze_vars (may use Variable.import_terms instead);
2006-07-12 haftmann 2006-07-12 added strip_abs_eta
2006-07-11 wenzelm 2006-07-11 removed obsolete xless; tuned zero_var_indexes;
2006-07-11 wenzelm 2006-07-11 removed obsolete ins_ix, mem_ix, ins_term, mem_term; moved variant(list), invent_names, bound, dest_internal/skolem etc. to name.ML;
2006-07-04 wenzelm 2006-07-04 added generalize/instantiate_option;
2006-06-17 wenzelm 2006-06-17 added exists_subtype; added internal/skolem (from Syntax/lexicon.ML); added generalize(T);
2006-05-16 wenzelm 2006-05-16 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 wenzelm 2006-04-26 tuned;
2006-04-24 haftmann 2006-04-24 cleaned up some diagnostic mathom
2006-04-10 wenzelm 2006-04-10 added aT (from axclass.ML); non-pervasive itselfT, a_itselfT;
2006-02-16 wenzelm 2006-02-16 tuned subst_bound(s);
2006-02-11 wenzelm 2006-02-11 added variant_name;
2006-02-10 wenzelm 2006-02-10 removed obsolete add_typ/term_classes/tycons;
2006-02-08 wenzelm 2006-02-08 map_type_tvar/tfree: map_atyps;
2006-02-08 haftmann 2006-02-08 fixed the most silly bug conceivable in map_atyps
2006-02-07 wenzelm 2006-02-07 lambda: base name of Const;
2006-02-06 wenzelm 2006-02-06 lambda: abstract over any const; tuned;
2006-02-06 haftmann 2006-02-06 added strip_abs
2006-02-02 wenzelm 2006-02-02 moved specific map_typ/term to sign.ML;
2006-01-31 wenzelm 2006-01-31 lambda: abstract over TYPE argument, too;
2006-01-30 haftmann 2006-01-30 added map_atype, map_aterms
2005-11-25 wenzelm 2005-11-25 added dummy_pattern;
2005-11-16 wenzelm 2005-11-16 added betapplys;
2005-11-10 wenzelm 2005-11-10 added find_free (from Isar/proof_context.ML);
2005-11-09 wenzelm 2005-11-09 removed obsolete term set operations;
2005-10-15 wenzelm 2005-10-15 tuned comments;
2005-10-07 wenzelm 2005-10-07 added absdummy;
2005-10-07 wenzelm 2005-10-07 added str_of_term (from HOL/Tools/ATP/recon_translate_proof.ML);
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-25 wenzelm 2005-09-25 zero_var_inst: replace loose bounds :000 etc.;