1997-02-14 paulson 1997-02-14 Added optimization: do nothing for empty list
1997-02-10 wenzelm 1997-02-10 fixed comment;
1997-02-06 wenzelm 1997-02-06 added eq_sort (will move to sorts.ML eventually); added get_sort (handles constraints / defaults); attach_types: adapted to new get_sort;
1996-11-28 paulson 1996-11-28 Tidying and renaming of function Dom
1996-11-26 paulson 1996-11-26 Removed or eta-expanded some declarations that are illegal under value polymorphism
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-01 paulson 1996-11-01 maxidx_of_typs replaces max o map maxidx_of_typ
1996-03-28 berghofe 1996-03-28 Optimized type inference (avoids chains of the form 'a |-> 'b |-> 'c ... in tye)
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-02-09 clasohm 1996-02-09 renamed expand_typ to norm_typ
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1996-01-11 nipkow 1996-01-11 Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.
1995-12-08 paulson 1995-12-08 infer_types now takes a term list and a type list as argument. It is defined using the new function infer_terms. Error messages and comments also improved.
1995-09-21 wenzelm 1995-09-21 added comment;
1995-09-01 wenzelm 1995-09-01 nonempty_sort: no longer var names as args;
1995-08-01 wenzelm 1995-08-01 added nonempty_sort (a somewhat braindead version!);
1995-03-17 nipkow 1995-03-17 Corrected a silly old bug in merge_tsigs. Rewrote a lot of Nimmermann's code.
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-09-26 wenzelm 1994-09-26 improved expand_typ (now handles TVars); slightly changed ext_tsig_abbrs; added ext_tsig_arities; removed extend_tsig; various internal changes;
1994-09-06 lcp 1994-09-06 Pure/type/unvarifyT: moved there from logic.ML
1994-09-06 wenzelm 1994-09-06 added ext_tsig_types; various minor changes;
1994-08-19 wenzelm 1994-08-19 slightly changed args of infer_types; replaced parents by enclose; renamed 2nd add_types to attach_types and fixed the typevar-sort-constraint BUG; various minor internal changes;
1994-07-06 wenzelm 1994-07-06 added raw_unify;
1994-06-16 wenzelm 1994-06-16 added ext_tsig_subclass, ext_tsig_defsort; minor internal rearrangements;
1994-06-09 wenzelm 1994-06-09 restored functor sig; added str_of_sort, str_of_arity, rem_sorts; minor internal cleanup;
1994-05-26 wenzelm 1994-05-26 replaced "logic" by logicC; added subsort, norm_sort;
1994-02-03 wenzelm 1994-02-03 (this is a preliminary release) type abbreviations;
1993-12-21 nipkow 1993-12-21 Necessary changes to accomodate type abbreviations.
1993-12-06 nipkow 1993-12-06 added rep_tsig
1993-11-29 nipkow 1993-11-29 added logical_types
1993-09-16 clasohm 1993-09-16 Initial revision