Fri, 14 Mar 1997 10:35:30 +0100 Avoid eta-contraction in the simplifier.
nipkow [Fri, 14 Mar 1997 10:35:30 +0100] rev 2792
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.
Tue, 11 Mar 1997 17:20:59 +0100 tuned glyphs;
wenzelm [Tue, 11 Mar 1997 17:20:59 +0100] rev 2791
tuned glyphs;
Tue, 11 Mar 1997 17:20:31 +0100 tuned Sigma glyph;
wenzelm [Tue, 11 Mar 1997 17:20:31 +0100] rev 2790
tuned Sigma glyph;
(0) -1000 -300 -100 -30 -10 -3 +3 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip