src/Pure/term.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.;
2005-09-08 haftmann 2005-09-08 introduces some modern-style AList operations
2005-09-06 haftmann 2005-09-06 introduced some new-style AList operations
2005-08-01 wenzelm 2005-08-01 removed atless (use term_ord instead); removed (inefficient) insert_aterm; improved bound: nameless, avoid allocating new strings; tuned sort_ord/typ_ord: dict_ord; tuned abstract_over: SAME; tuned add_term_vars/frees: OrdList.insert; removed compress_type/compress_type (cf. compress.ML);
2005-07-28 wenzelm 2005-07-28 added add_tfreesT, add_tfrees; added bound; added zero_var_indexesT, zero_var_indexes, zero_var_indexes_subst; removed add_term_constsT; tuned;
2005-07-19 wenzelm 2005-07-19 moved incr_tvar to logic.ML; added eq_var, eq_tvar, instantiate, instantiateT;
2005-07-15 wenzelm 2005-07-15 replaced foldl_XXX by canonical fold_XXX; canonical arguments for add_term_varnames, add_tvarsT, add_tvars, add_vars, add_frees,
2005-07-13 wenzelm 2005-07-13 fixed comment-out;
2005-07-13 haftmann 2005-07-13 (fix for an accidental commit)
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-07-06 wenzelm 2005-07-06 tuned eq_ix;
2005-07-06 wenzelm 2005-07-06 tuned maxidx_of_typ/typs/term; moved adhoc string_of_term to HOL/Tools/ATP/recon_translate_proof.ML; cleaned signature;
2005-07-04 wenzelm 2005-07-04 added fast_indexname_ord, fast_term_ord; changed sort_ord, typ_ord, Vartab, Termtab: use fast orders; added argument_type_of, dest_abs; tuned;
2005-07-01 wenzelm 2005-07-01 tuned term_ord: less garbage;
2005-06-29 wenzelm 2005-06-29 tuned sort_ord: pointer_eq; tuned size_of_term: less stack usage;
2005-06-28 paulson 2005-06-28 first-order check now allows quantifiers
2005-06-25 nipkow 2005-06-25 Added term_lpo
2005-06-22 wenzelm 2005-06-22 export sort_ord; tuned term_ord, typ_ord: use pointer_eq; tuned aconv, aconvs: based on term_ord;
2005-06-09 wenzelm 2005-06-09 map_typ and map_term no longer global;
2005-06-06 wenzelm 2005-06-06 avoid polymorphic ins;
2005-05-29 obua 2005-05-29 Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
2005-05-22 wenzelm 2005-05-22 added show_dummy_patterns;
2005-05-17 wenzelm 2005-05-17 renamed show_var_qmarks to show_question_marks; string_of_vname: improved treatment of \<^isub> and \<^isup>;
2005-05-16 kleing 2005-05-16 line wrap