src/Pure/term.ML
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
2005-05-12 paulson 2005-05-12 first-order now ignores "all"
2005-05-03 dixon 2005-05-03 lucas - added dest_TVar and dest_TFree.
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-03-26 gagern 2005-03-26 op vor infix-Konstruktoren im datatype binding zum besseren Parsen
2005-03-17 nipkow 2005-03-17 added string_of_term
2005-03-10 ballarin 2005-03-10 Registrations of global locale interpretations: improved, better naming.
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-04 paulson 2005-03-04 new first_order test
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-27 berghofe 2005-01-27 Added show_var_qmarks flag.
2004-07-08 wenzelm 2004-07-08 added add_term_varnames, term_varnames;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-29 wenzelm 2004-05-29 moved read_int etc. to library.ML; added type 'arity';
2004-05-21 wenzelm 2004-05-21 moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
2004-05-01 wenzelm 2004-05-01 improved Term.invent_names;
2004-04-26 wenzelm 2004-04-26 variant: use Symbol.bump_init;
2004-03-19 paulson 2004-03-19 Removing the datatype declaration of "order" allows the standard General.order to be used. Thus we can use Int.compare and String.compare instead of the slower home-grown versions.
2002-10-21 berghofe 2002-10-21 - removed flexpair - added maxidx_of_terms - tuned lambda: now also abstracts over Vars
2002-10-14 nipkow 2002-10-14 Ported find_intro/elim to Isar.
2002-08-08 wenzelm 2002-08-08 adhoc_freeze_vars;
2002-03-01 wenzelm 2002-03-01 structure Typtab; clarified typ_ord; clarified compress_type;
2002-02-28 wenzelm 2002-02-28 added match_bvars, rename_abs (from thm.ML);
2002-02-20 wenzelm 2002-02-20 Symbol.bump_string;
2002-01-17 wenzelm 2002-01-17 added add_term_free_names (more precise/efficient than add_term_names);