src/Pure/term.ML
2010-09-13 wenzelm 2010-09-13 tuned;
2010-09-02 wenzelm 2010-09-02 turned show_question_marks into proper configuration option; show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname; tuned;
2010-03-27 wenzelm 2010-03-27 added Term.fold_atyps_sorts convenience;
2010-02-19 haftmann 2010-02-19 added dest_comb
2010-01-28 wenzelm 2010-01-28 tuned signature;
2009-11-15 wenzelm 2009-11-15 tuned;
2009-11-09 wenzelm 2009-11-09 locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-26 wenzelm 2009-07-26 lambda/cabs/all: named variants;
2009-07-16 wenzelm 2009-07-16 use structure Same; tuned;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 close_schematic_term: uniform order of types/terms; tuned;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2009-02-27 wenzelm 2009-02-27 tuned/unified size_of_term and size_of_typ, eliminated obsolete foldl;
2009-02-13 kleing 2009-02-13 New command find_consts searching for constants by type (by Timothy Bourke).
2009-01-01 wenzelm 2009-01-01 added canonical add_const_names, add_consts;
2008-12-31 wenzelm 2008-12-31 updated header;
2008-12-31 wenzelm 2008-12-31 added declare_term_frees; tuned signature;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-30 wenzelm 2008-12-30 provide canonical add_tvar_namesT, add_tvar_names, add_tfree_namesT, add_tfree_names, add_free_names; renamed add_varnames to add_var_names; removed old add_typ_ixns, add_term_tvar_ixns;
2008-12-30 wenzelm 2008-12-30 removed unused head_name_of; tuned;
2008-06-23 wenzelm 2008-06-23 moved implies to logic.ML; removed equals; qualified all;
2007-10-16 wenzelm 2007-10-16 tuned hidden_polymorphism; added close_schematic_term;
2007-10-11 wenzelm 2007-10-11 replaced Term.equiv_types by Type.similar_types;
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.