src/Pure/unify.ML
2012-07-15 wenzelm 2012-07-15 prefer canonical fold_rev;
2012-07-15 wenzelm 2012-07-15 back to naive insertion sort before 1997 to accommodate peculiar less_arg relation -- NB: make_ord arg_less was not a quasi-order and thus inappropriate for generic sort (cf. de74b549f976, ecfeff48bf0c);
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-04-07 wenzelm 2011-04-07 constant =?= no longer exists (cf. 8c09e1fa24a7);
2010-12-30 wenzelm 2010-12-30 uniform treatment of type vs. term environment (cf. b654fa27fbc4); tuned;
2010-10-15 paulson 2010-10-15 prevention of self-referential type environments
2010-09-06 wenzelm 2010-09-06 more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
2010-09-03 wenzelm 2010-09-03 more explicit Config.declare vs. Config.declare_global;
2010-07-05 paulson 2010-07-05 Unification (flexflex) bug fix; making "auto" deterministic
2010-06-29 wenzelm 2010-06-29 fail with low-level exception, not user error;
2010-06-29 wenzelm 2010-06-29 eliminated some unused bindings;
2010-06-29 wenzelm 2010-06-29 recovered some indentation from the depths of time;
2010-05-10 wenzelm 2010-05-10 renamed Config.get_thy to Config.get_global etc. to indicate that this is not the real thing;
2010-03-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-22 haftmann 2009-10-22 map_range (and map_index) combinator
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-09-09 paulson 2008-09-09 Increasing the default limits in order to prevent unnecessary failures.
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-03-19 haftmann 2008-03-19 Type.lookup now curried
2007-08-07 wenzelm 2007-08-07 turned Unify flags into configuration options (global only);
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2006-09-21 wenzelm 2006-09-21 member (op =);
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 removed obsolete xless;
2006-07-11 wenzelm 2006-07-11 removed obsolete mem_ix;
2006-07-06 wenzelm 2006-07-06 matchers: fall back on plain first_order_matchers, not pattern;
2006-06-19 wenzelm 2006-06-19 matchers: try pattern_matchers only *after* general matching (The pattern version is not a faithful approximation because it falls back on first-order matching!);
2006-06-13 wenzelm 2006-06-13 tuned;
2006-06-12 wenzelm 2006-06-12 tuned;
2006-06-12 wenzelm 2006-06-12 added matchers, matches_list; tuned interfaces;
2006-04-26 wenzelm 2006-04-26 tuned;
2006-02-06 wenzelm 2006-02-06 moved combound, rlist_abs to logic.ML;
2005-11-16 wenzelm 2005-11-16 tuned Pattern.match/unify;
2005-09-13 wenzelm 2005-09-13 Seq.maps;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify;
2005-07-01 wenzelm 2005-07-01 back to 1.28;
2005-06-30 wenzelm 2005-06-30 revert to 1.27 due to obscure performance issues (!??);
2005-06-29 wenzelm 2005-06-29 pass thy as explicit argument (the old ref was not safe in conjunction with lazy evaluation -- the unify code could be fooled about the present theory context);
2005-06-17 wenzelm 2005-06-17 accomodate identification of type Sign.sg and theory;
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-11-11 paulson 2004-11-11 increased tracing and search bounds
2004-04-22 wenzelm 2004-04-22 tuned;
2001-12-18 wenzelm 2001-12-18 tuned Type.unify;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-19 berghofe 2001-11-19 Moved head_norm and fastype from unify.ML to envir.ML
2000-03-10 berghofe 2000-03-10 Type.unify and Type.typ_match now use Vartab instead of association lists.
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-27 wenzelm 1997-11-27 fixed warning;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-10-24 wenzelm 1997-10-24 ProtoPure.thy;
1997-03-07 paulson 1997-03-07 Removed some polymorphic equality tests
1996-11-18 paulson 1996-11-18 Changed subst_bounds to subst_bound, to run faster
1996-11-12 paulson 1996-11-12 Changed some mem calls to be monomorphic