src/Pure/type.ML
2006-10-31 haftmann 2006-10-31 fixed type signature of Type.varify
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-09-21 wenzelm 2006-09-21 serial numbers for types;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-05-22 wenzelm 2006-05-22 export raw_unifys, could_unifys;
2006-05-20 wenzelm 2006-05-20 export raw_matches;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-05-05 wenzelm 2006-05-05 replaced Sorts.DOMAIN by general Sorts.CLASS_ERROR; add_types etc.: reject qualified dummy types -- prevents users from messing up some internal conventions;
2006-05-02 wenzelm 2006-05-02 tuned;
2006-04-30 wenzelm 2006-04-30 build classes/arities: refer to operations in sorts.ML; simplified add_class/classrel/arity; tuned;
2006-04-25 wenzelm 2006-04-25 added inter_sort; added arity_number/sorts;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-03-11 wenzelm 2006-03-11 got rid of type Sign.sg;
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 TableFun: renamed xxx_multi to xxx_list; tuned;
2006-02-06 haftmann 2006-02-06 subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
2005-10-08 wenzelm 2005-10-08 added could_unify;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-29 wenzelm 2005-08-29 use AList operations;
2005-07-28 wenzelm 2005-07-28 typ_match, unify: canonical argument order; added raw_match, raw_instance; proper implementation of raw_unify;
2005-07-19 wenzelm 2005-07-19 tuned match, unify;
2005-07-01 berghofe 2005-07-01 Moved eq_type from envir.ML to type.ML
2005-06-17 wenzelm 2005-06-17 Symtab.fold;
2005-06-11 wenzelm 2005-06-11 name space of classes and types maintained in tsig;
2005-06-09 wenzelm 2005-06-09 renamed cert_typ_raw to cert_typ_abbrev; renamed add_abbrs to add_abbrevs; tuned;
2005-06-05 wenzelm 2005-06-05 added Type.freeze(_type); tuned;
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;