2007-08-07 ago turned Unify flags into configuration options (global only);
2007-05-31 ago simplified/unified list fold;
2006-09-21 ago member (op =);
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-11 ago removed obsolete xless;
2006-07-11 ago removed obsolete mem_ix;
2006-07-06 ago matchers: fall back on plain first_order_matchers, not pattern;
2006-06-19 ago matchers: try pattern_matchers only *after* general matching (The
2006-06-13 ago tuned;
2006-06-12 ago tuned;
2006-06-12 ago added matchers, matches_list;
2006-04-26 ago tuned;
2006-02-06 ago moved combound, rlist_abs to logic.ML;
2005-11-16 ago tuned Pattern.match/unify;
2005-09-13 ago Seq.maps;
2005-07-28 ago Sign.typ_unify;
2005-07-01 ago back to 1.28;
2005-06-30 ago revert to 1.27 due to obscure performance issues (!??);
2005-06-29 ago pass thy as explicit argument (the old ref was not safe
2005-06-17 ago accomodate identification of type and theory;
2005-04-21 ago - Eliminated nodup_vars check.
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2004-11-11 ago increased tracing and search bounds
2004-04-22 ago tuned;
2001-12-18 ago tuned Type.unify;
2001-11-21 ago use tracing function for trace output;
2001-11-19 ago Moved head_norm and fastype from unify.ML to envir.ML
2000-03-10 ago Type.unify and Type.typ_match now use Vartab instead of association lists.
1997-12-19 ago adapted to new sort function;
1997-11-27 ago fixed warning;
1997-11-21 ago changed Sequence interface (now Seq, in seq.ML);
1997-10-24 ago ProtoPure.thy;
1997-03-07 ago Removed some polymorphic equality tests
1996-11-18 ago Changed subst_bounds to subst_bound, to run faster
1996-11-12 ago Changed some mem calls to be monomorphic
1996-10-30 ago Changed some mem calls to mem_int for greater efficiency (not that it could matter)
1996-02-16 ago Elimination of fully-functorial style.
1996-01-29 ago inserted tabs again
1996-01-29 ago removed tabs
1996-01-11 ago Removed bug in type unification. Negative indexes are not used any longer.
1995-03-03 ago added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1994-10-21 ago Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
1994-10-19 ago new comments explaining abandoned change
1993-09-16 ago Initial revision