# HG changeset patch
# User wenzelm
# Date 863790624 -7200
# Node ID 567c093297e6ef65851da5035c2422fc29c1b759
# Parent  57a9b613036edb76545416ba648b7ee35cdf38ba
hint at more sections;
named infixes;

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