1.1 --- a/doc-src/Intro/advanced.tex	Fri May 16 15:49:27 1997 +0200
     1.2 +++ b/doc-src/Intro/advanced.tex	Fri May 16 15:50:24 1997 +0200
     1.3 @@ -355,11 +355,12 @@
     1.4  rewrite rules on abstract syntax trees, handling notations and
     1.5  abbreviations.  \index{*ML section} The {\tt ML} section may contain
     1.6  code to perform arbitrary syntactic transformations.  The main
     1.7 -declaration forms are discussed below.  The full syntax can be found
     1.8 -in \iflabelundefined{app:TheorySyntax}{an appendix of the {\it
     1.9 -    Reference Manual}}{App.\ts\ref{app:TheorySyntax}}.  Also note that
    1.10 -object-logics may add further theory sections, for example {\tt
    1.11 -  typedef}, {\tt datatype} in \HOL.
    1.12 +declaration forms are discussed below.  There are some more sections
    1.13 +not presented here, the full syntax can be found in
    1.14 +\iflabelundefined{app:TheorySyntax}{an appendix of the {\it Reference
    1.15 +    Manual}}{App.\ts\ref{app:TheorySyntax}}.  Also note that
    1.16 +object-logics may add further theory sections, for example
    1.17 +\texttt{typedef}, \texttt{datatype} in \HOL.
    1.18  
    1.19  All the declaration parts can be omitted or repeated and may appear in
    1.20  any order, except that the {\ML} section must be last (after the {\tt
    1.21 @@ -620,6 +621,12 @@
    1.22  \verb|op #(True) == op ~&(True)|, which asserts that the functions $\lambda
    1.23  Q.True \xor Q$ and $\lambda Q.True \nand Q$ are identical.
    1.24  
    1.25 +\medskip Infix syntax and constant names may be also specified
    1.26 +independently. For example, consider this version of $\nand$:
    1.27 +\begin{ttbox}
    1.28 +consts  nand     :: [o,o] => o         (infixl "~&" 35)
    1.29 +\end{ttbox}
    1.30 +
    1.31  \bigskip\index{mixfix declarations}
    1.32  {\bf Mixfix} operators may have arbitrary context-free syntaxes.  Let us
    1.33  add a line to the constant declaration part: