src/Pure/unify.ML
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-26 wenzelm 2014-03-26 prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;
2013-07-18 wenzelm 2013-07-18 guard unify tracing via visible status of global theory; find_theorems: back-patching of background theory to observe Context_Position.is_visible avoids spamming via auto solve_direct;
2013-07-18 wenzelm 2013-07-18 tuned;
2013-05-29 wenzelm 2013-05-29 tuned signature;
2013-05-29 wenzelm 2013-05-29 backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;
2013-05-27 wenzelm 2013-05-27 more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);
2013-05-24 wenzelm 2013-05-24 tuned signature -- slightly more general operations (cf. term.ML);
2013-05-24 wenzelm 2013-05-24 re-use Pattern.unify_types, including its trace_unify_fail option;
2013-05-24 wenzelm 2013-05-24 tuned signature; tuned comments;
2013-04-12 wenzelm 2013-04-12 tuned signature; tuned comments;
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;