src/Pure/pattern.ML
2013-07-19 wenzelm 2013-07-19 turned pattern unify flag into configuration option (global only);
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 proper internal error, not user error;
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-05-24 wenzelm 2013-05-24 tuned;
2013-05-24 wenzelm 2013-05-24 unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");
2013-05-24 wenzelm 2013-05-24 re-use Pattern.unify_types, including its trace_unify_fail option;
2013-04-12 wenzelm 2013-04-12 tuned signature; tuned comments;
2012-03-10 wenzelm 2012-03-10 clarified Pattern.matchess;
2012-01-14 wenzelm 2012-01-14 discontinued old-style Term.list_abs in favour of plain Term.abs;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2010-12-07 wenzelm 2010-12-07 eliminated some hard tabulators (deprecated);
2010-11-26 wenzelm 2010-11-26 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
2010-11-19 paulson 2010-11-19 First-order pattern matching: catch a rogue exception (differing numbers of arguments)
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-18 berghofe 2010-02-18 Added function rewrite_term_top for top-down rewriting.
2009-10-21 haftmann 2009-10-21 curried inter as canonical list operation (beware of argument order)
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir operations;
2009-03-17 wenzelm 2009-03-17 export match_rew -- useful for implementing "procs" for rewrite_term;
2009-03-17 wenzelm 2009-03-17 tuned aeconv: test plain aconv before expensive eta_contract;
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-25 haftmann 2008-09-25 matchess
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-05-07 berghofe 2008-05-07 - Removed function eta_contract_atom, which did not quite work - Corrected and simplified function aeconv
2007-11-27 berghofe 2007-11-27 first_order_match now only calls loose_bvar when inside an abstraction.
2007-06-03 wenzelm 2007-06-03 added downto0 (from library.ML);
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-02-06 wenzelm 2007-02-06 tuned matches_subterm;
2006-09-21 wenzelm 2006-09-21 member (op =); tuned pattern check;
2006-07-11 wenzelm 2006-07-11 removed obsolete xless;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.bound;
2006-06-13 wenzelm 2006-06-13 added equiv;
2006-06-12 wenzelm 2006-06-12 removed matches_seq -- didn't quite work;
2006-06-05 wenzelm 2006-06-05 added matches_seq (left-to-right matching, intermediate beta-normalization);
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-21 wenzelm 2006-03-21 subtract (op =);
2006-02-06 wenzelm 2006-02-06 moved (beta_)eta_contract to envir.ML; tuned;
2005-11-16 wenzelm 2005-11-16 tuned interfaces to support incremental match/unify (cf. versions in type.ML);
2005-10-28 haftmann 2005-10-28 cleaned up nth, nth_update, nth_map and nth_string functions
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
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-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-01 wenzelm 2005-08-01 nameless Term.bound;
2005-07-28 wenzelm 2005-07-28 Sign.typ_unify; Term.bound; tuned rewrite_term;
2005-07-01 wenzelm 2005-07-01 avoid polyeq;
2005-07-01 berghofe 2005-07-01 Changed interface of Envir.lookup'
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-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-05 wenzelm 2004-06-05 avoid implicit arguments via refs;
2004-06-01 berghofe 2004-06-01 Removed ~10000 hack in function idx that can lead to inconsistencies when unifying terms with a large number of abstractions.