1.1 --- a/doc-src/Ref/introduction.tex	Fri Apr 22 18:08:57 1994 +0200
     1.2 +++ b/doc-src/Ref/introduction.tex	Fri Apr 22 18:18:37 1994 +0200
     1.3 @@ -142,7 +142,7 @@
     1.4  
     1.5  \begin{ttdescription}
     1.6  \item[\ttindexbold{show_hyps} := false;]   
     1.7 -makes Isabelle show each meta-level hypotheses as a dot.
     1.8 +makes Isabelle show each meta-level hypothesis as a dot.
     1.9  
    1.10  \item[\ttindexbold{show_types} := true;]
    1.11  makes Isabelle show types when printing a term or theorem.
    1.12 @@ -160,7 +160,7 @@
    1.13  The {\bf $\eta$-contraction law} asserts $(\lambda x.f(x))\equiv f$,
    1.14  provided $x$ is not free in ~$f$.  It asserts {\bf extensionality} of
    1.15  functions: $f\equiv g$ if $f(x)\equiv g(x)$ for all~$x$.  Higher-order
    1.16 -unification occasionally puts terms into a fully $\eta$-expanded form.  For
    1.17 +unification frequently puts terms into a fully $\eta$-expanded form.  For
    1.18  example, if $F$ has type $(\tau\To\tau)\To\tau$ then its expanded form is
    1.19  $\lambda h.F(\lambda x.h(x))$.  By default, the user sees this expanded
    1.20  form.