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