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-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
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
1994-01-18 nipkow 1994-01-18 some optimizations of Larry's
1994-01-14 nipkow 1994-01-14 optimized net for matching of abstractions to speed up simplifier
1993-09-16 clasohm 1993-09-16 Initial revision