# HG changeset patch
# User lcp
# Date 754315235 -3600
# Node ID c2fcb6c07689222eca292c0ebb2e3d5a8763fc5f
# Parent  8258c26ae0845a311346f3e1ec0dddcc9092255c
Correction to eta-contraction; thanks to Markus W.

diff -r 8258c26ae084 -r c2fcb6c07689 doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Fri Nov 26 12:54:58 1993 +0100
+++ b/doc-src/Ref/introduction.tex	Fri Nov 26 13:00:35 1993 +0100
@@ -198,9 +198,10 @@
 The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
 provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
 functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
-unification puts terms into a fully $\eta$-expanded form.  For example, if
-$F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is $\lambda
-h.F(\lambda x.h(x))$.  By default, the user sees this expanded form.
+unification occasionally puts terms into a fully $\eta$-expanded form.  For
+example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
+$\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
+form.
 
 \begin{description}
 \item[\ttindexbold{eta_contract} \tt:= true;]