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