src/Pure/type.ML
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-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-06-22 wenzelm 2004-06-22 tuned;
2004-06-22 wenzelm 2004-06-22 tuned certify_typ/term;
2004-06-21 wenzelm 2004-06-21 tuned certify_typ;
2004-06-09 wenzelm 2004-06-09 tuned messages;
2004-05-29 wenzelm 2004-05-29 removed norm_typ; improved output; refer to Pretty.pp;
2004-05-21 wenzelm 2004-05-21 major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
2002-10-21 berghofe 2002-10-21 Removed add_env because Vartab.map was too slow for large environments.
2002-01-12 wenzelm 2002-01-12 paramify_dummies: proper treatment of maxidx;
2001-12-18 wenzelm 2001-12-18 tuned interface of unify, param; added paramify_dummies to turn TypeInfer.anyT into unifiable parameter;
2001-12-14 wenzelm 2001-12-14 varify returns newly introduced variables;
2001-11-28 wenzelm 2001-11-28 Syntax.typ_of_term: pass intern sort fn;
2001-11-16 wenzelm 2001-11-16 ext_tsig_classes: rebuild_tsig!!!!!
2001-02-01 wenzelm 2001-02-01 ext_classrel: certify_class;
2000-11-18 wenzelm 2000-11-18 export freeze_thaw_type;
2000-08-03 wenzelm 2000-08-03 typ_no_norm;
2000-05-21 wenzelm 2000-05-21 removed is_type_abbr;
2000-04-17 wenzelm 2000-04-17 NameSpace.is_qualified;
2000-04-14 wenzelm 2000-04-14 added is_type_abbr;
2000-03-30 wenzelm 2000-03-30 tuned;
2000-03-10 berghofe 2000-03-10 Type.unify and Type.typ_match now use Vartab instead of association lists.
1999-09-29 wenzelm 1999-09-29 added witness_sorts, univ_witness; removed nonempty_sort; tsig: log_types, univ_witness (require rebuild_tsig!); heavily tuned;
1999-08-18 paulson 1999-08-18 freeze_thaw does nothing if no variables
1999-07-23 wenzelm 1999-07-23 replaced assoc lists by Symtab.table;
1998-08-19 wenzelm 1998-08-19 fixed param;
1998-06-25 wenzelm 1998-06-25 defaults for free variables hide consts of same name;
1998-05-28 wenzelm 1998-05-28 fixed error msgs;
1998-02-05 wenzelm 1998-02-05 added param;
1997-11-05 wenzelm 1997-11-05 fixed exception OPTION;
1997-10-10 wenzelm 1997-10-10 decode: qualified is always const;
1997-10-07 wenzelm 1997-10-07 tuned decode;
1997-10-06 wenzelm 1997-10-06 eliminated raise_term, raise_typ; tuned get_sort, decode_types, infer_types to accomodate qualified names;
1997-06-05 paulson 1997-06-05 Removal of freeze_vars and thaw_vars. New freeze_thaw
1997-05-13 wenzelm 1997-05-13 of_sort: type_sig -> typ * sort -> bool;
1997-04-18 wenzelm 1997-04-18 tuned check_has_sort; fixed norm_typ: also does norm_sort;
1997-04-17 wenzelm 1997-04-17 improved type check error messages;
1997-04-16 wenzelm 1997-04-16 moved classes / sorts to sorts.ML; moved (and reimplemented) type inference to type_infer.ML; cleaned up type unification; misc cleanup and tuning;
1997-03-07 paulson 1997-03-07 Removed some polymorphic equality tests
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
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.