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