| changeset 9231 | 8812a07d52ee |
| parent 8908 | 25f2bdc02123 |
| child 9695 | ec7d7f877712 |
--- a/doc-src/Ref/introduction.tex Sat Jul 01 19:55:22 2000 +0200 +++ b/doc-src/Ref/introduction.tex Sat Jul 01 19:56:46 2000 +0200 @@ -301,7 +301,7 @@ \subsection{Eta-contraction before printing} \begin{ttbox} -eta_contract: bool ref \hfill{\bf initially false} +eta_contract: bool ref \end{ttbox} The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$, provided $x$ is not free in ~$f$. It asserts {\bf extensionality} of