src/Pure/term.ML
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);
2001-12-14 wenzelm 2001-12-14 added invent_type_names; added add_tvarsT etc. (from drule.ML);
2001-11-28 wenzelm 2001-11-28 variant: preserve suffix of underscores (for skolem/internal names etc.);
2001-10-24 wenzelm 2001-10-24 added lambda;
2001-10-23 wenzelm 2001-10-23 replace_dummy_patterns: lift over bounds;
2001-05-31 wenzelm 2001-05-31 invent_names
2001-01-06 wenzelm 2001-01-06 added list_abs;
2000-12-13 wenzelm 2000-12-13 fixed add_term_names: NameSpace.base;
2000-11-30 wenzelm 2000-11-30 added is_replaced_dummy_pattern;
2000-08-29 nipkow 2000-08-29 *** empty log message ***
2000-08-04 wenzelm 2000-08-04 added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
2000-07-13 wenzelm 2000-07-13 add_term_consts: ins_string;
2000-03-30 wenzelm 2000-03-30 foldl_term_types: depend on term as well;
2000-03-10 berghofe 2000-03-10 Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
1999-09-29 wenzelm 1999-09-29 added rems_sort;
1999-09-01 wenzelm 1999-09-01 structure Termtab;
1999-08-23 nipkow 1999-08-23 Corrected two busg in the simplifier.
1999-07-10 wenzelm 1999-07-10 Symtab.lookup_multi;
1999-04-30 wenzelm 1999-04-30 val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
1998-12-18 paulson 1998-12-18 moved dest_Type to term.ML from HOL/Tools/primrec_package
1998-11-29 wenzelm 1998-11-29 added oct_char;
1998-09-29 paulson 1998-09-29 new function inter_term
1998-03-09 wenzelm 1998-03-09 tuned some names;
1998-02-18 nipkow 1998-02-18 Improved loop-test for rewrite rules a little. Should be done properly!
1998-02-12 wenzelm 1998-02-12 tuned comments;
1998-02-06 wenzelm 1998-02-06 added Vartab: TABLE;
1997-12-28 wenzelm 1997-12-28 made MLWorks happy;
1997-12-28 wenzelm 1997-12-28 renamed Symtab.null to Symtab.empty;
1997-12-24 wenzelm 1997-12-24 export range_type;
1997-12-22 paulson 1997-12-22 Added range-type for completeness
1997-12-19 wenzelm 1997-12-19 term order; signature;
1997-11-26 wenzelm 1997-11-26 added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a; added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a; added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;
1997-11-07 oheimb 1997-11-07 changed libraray function find to find_index_eq, currying it