1.1 --- a/doc-src/Intro/advanced.tex	Mon May 05 18:09:31 1997 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Mon May 05 18:50:26 1997 +0200
     1.3 @@ -368,7 +368,7 @@
     1.4  theories, inheriting their types, constants, syntax, etc.  The theory
     1.5  \thydx{Pure} contains nothing but Isabelle's meta-logic. The variant
     1.6  \thydx{CPure} offers the more usual higher-order function application
     1.7 -syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$.
     1.8 +syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$ in \Pure.
     1.9  
    1.10  Each theory definition must reside in a separate file, whose name is
    1.11  the theory's with {\tt.thy} appended.  Calling
    1.12 @@ -429,9 +429,9 @@
    1.13  the keyword {\tt defs} instead of {\tt rules}.  {\bf Definitions} are
    1.14  rules of the form $s \equiv t$, and should serve only as
    1.15  abbreviations. The simplest form of a definition is $f \equiv t$,
    1.16 -where $f$ is a constant. Also allowed are $\eta$-equivalent forms,
    1.17 -where the arguments of~$f$ appear applied on the left-hand side of the
    1.18 -equation instead of abstracted on the right-hand side.
    1.19 +where $f$ is a constant. Also allowed are $\eta$-equivalent forms of
    1.20 +this, where the arguments of~$f$ appear applied on the left-hand side
    1.21 +of the equation instead of abstracted on the right-hand side.
    1.22  
    1.23  Isabelle checks for common errors in definitions, such as extra
    1.24  variables on the right-hand side, but currently does not a complete