src/Pure/term.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
1997-11-07 oheimb 1997-11-07 added exists_Const
1997-11-01 paulson 1997-11-01 New syntax function for types
1997-10-28 wenzelm 1997-10-28 add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons, add_term_consts, map_typ, map_term: moved from sign.ML to term.ML;
1997-10-21 wenzelm 1997-10-21 made Poly/ML happy, but SML/NJ unhappy;
1997-10-20 wenzelm 1997-10-20 make SML/NJ happy;
1997-10-06 wenzelm 1997-10-06 eliminated raise_term;
1997-04-16 wenzelm 1997-04-16 tuned type of eq_ix, mem_ix;
1997-03-14 nipkow 1997-03-14 Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.
1997-03-07 paulson 1997-03-07 Improved indentation of aconv
1997-02-04 paulson 1997-02-04 Gradual switching to Basis Library functions nth, drop, etc.
1996-11-18 paulson 1996-11-18 Optimizations: removal of polymorphic equality; one-argument case for subst_bounds
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-12 paulson 1996-11-12 Changed some mem and ins calls to be monomorphic
1996-11-01 paulson 1996-11-01 maxidx_of_typs replaces max o map maxidx_of_typ Now uses Int.max instead of max
1996-10-30 paulson 1996-10-30 Changed some mem calls to mem_string for greater efficiency (not that it could matter)
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1995-12-28 paulson 1995-12-28 Updated comments for compression functions
1995-12-22 paulson 1995-12-22 Addition of compression, that is, sharing. Uses refs and Symtab (binary search trees) to get reasonable speed. Types and terms can be compressed.
1995-12-08 paulson 1995-12-08 type_of1: improved error messages
1995-11-23 clasohm 1995-11-23 files now define a structure to allow SML/NJ to optimize the code
1995-04-12 nipkow 1995-04-12 term.ML: add_loose_bnos now returns a list w/o duplicates. pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)
1995-03-13 nipkow 1995-03-13 Changed treatment of during type inference internally generated type variables. 1. They are renamed to 'a, 'b, 'c etc away from a given set of used names. 2. They are either frozen (turned into TFrees) or left schematic (TVars) depending on a parameter. In goals they are frozen, for instantiations they are left schematic.
1994-11-22 lcp 1994-11-22 Pure/term: commented typ_subst_TVars, subst_TVars, subst_Vars, subst_vars
1994-05-18 wenzelm 1994-05-18 added logicC: class, logicS: sort; added itselfT: typ -> typ, a_itselfT: typ (for axclasses);
1993-10-21 lcp 1993-10-21 Pure/term/fastype_of1: renamed from fastype_of Pure/term/fastype_of: new, takes only one argument (like type_of) Pure/Syntax/printer/is_prop: now calls fastype_of1 Pure/pattern: now calls new fastype_of in three places Pure/logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of. So it no longer checks t properly -- but it never checked u anyway, and all existing calls are derived from certified terms...
1993-10-08 wenzelm 1993-10-08 added raise_type: string -> typ list -> term list -> 'a; added raise_term: string -> term list -> 'a;
1993-09-16 clasohm 1993-09-16 Initial revision