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.
2004-05-21 wenzelm 2004-05-21 adapted tsig interface;
2004-04-22 wenzelm 2004-04-22 tuned;
2003-05-10 berghofe 2003-05-10 Added new function eta_long.
2003-04-04 berghofe 2003-04-04 type_of_G now applies type substitution before decomposing type.
2002-10-11 berghofe 2002-10-11 norm_typ -> Envir.norm_type
2002-10-10 nipkow 2002-10-10 added failure trace information to pattern unification
2002-05-31 berghofe 2002-05-31 Changes to rewrite_term: - now uses skeletons to speed up rewriting - added interface for rewriting procedures
2002-02-28 wenzelm 2002-02-28 rewrite_term: Term.rename_abs;
2002-01-21 berghofe 2002-01-21 Removed timing function.
2002-01-18 wenzelm 2002-01-18 rewrite_term: removed rew0, so no on-the-fly eta-contraction;
2002-01-17 wenzelm 2002-01-17 eta_contract with sharing (by berghofe); rewrite_term: proper handling of Abs cong;
2002-01-16 wenzelm 2002-01-16 added rewrite_term; tuned; GPLed;
2002-01-16 wenzelm 2002-01-16 added beta_eta_contract;
2001-12-18 wenzelm 2001-12-18 tuned Type.unify;
2001-11-19 berghofe 2001-11-19 Replaced devar by Envir.head_norm
2000-03-10 berghofe 2000-03-10 Type.unify and Type.typ_match now use Vartab instead of association lists.
1999-04-29 nipkow 1999-04-29 Eta contraction is now performed all the time during rewriting.
1998-04-22 nipkow 1998-04-22 Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching.
1998-02-28 nipkow 1998-02-28 Tried to reorganize rewriter a little. More to be done.
1997-03-14 nipkow 1997-03-14 Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.
1997-03-07 paulson 1997-03-07 Corrected aeconv and exported it
1997-03-05 paulson 1997-03-05 Declares eta_contract_atom; fixed comment; some tidying
1997-02-14 paulson 1997-02-14 A bit more pattern-matching in eta_contract
1996-11-26 paulson 1996-11-26 Removal of needless function definition
1996-03-14 berghofe 1996-03-14 Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1996-01-11 nipkow 1996-01-11 Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.
1995-04-12 nipkow 1995-04-12 term.ML: add_loose_bnos now returns a list w/o duplicates. pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)
1994-11-02 nipkow 1994-11-02 Modified pattern.ML to perform proper matching of Higher-Order Patterns. Modified thm.ML to preserve bound var names during rewriting. Renamed eta_matches to matches.
1993-10-21 lcp 1993-10-21 now calls new fastype_of in three places
1993-09-16 clasohm 1993-09-16 Initial revision