1.1 --- a/doc-src/Ref/defining.tex	Fri Apr 14 11:27:18 1995 +0200
     1.2 +++ b/doc-src/Ref/defining.tex	Fri Apr 14 11:27:57 1995 +0200
     1.3 @@ -384,25 +384,6 @@
     1.4  pretty printing.  Special case annotations provide a simple means of
     1.5  specifying infix operators and binders.
     1.6  
     1.7 -
     1.8 -%% FIXME remove
     1.9 -%\subsection{Grammar productions}\label{sec:grammar}\index{productions}
    1.10 -%
    1.11 -%Let us examine the treatment of the production
    1.12 -%\[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\, A@2^{(p@2)}\, \ldots\,
    1.13 -%                  A@n^{(p@n)}\, w@n. \]
    1.14 -%Here $A@i^{(p@i)}$ is a nonterminal with priority~$p@i$ for $i=1$,
    1.15 -%\ldots,~$n$, while $w@0$, \ldots,~$w@n$ are strings of terminals.
    1.16 -%In the corresponding mixfix annotation, the priorities are given separately
    1.17 -%as $[p@1,\ldots,p@n]$ and~$p$.  The nonterminal symbols are derived from
    1.18 -%types~$\tau$, $\tau@1$, \ldots,~$\tau@n$ respectively, and the production's
    1.19 -%effect on nonterminals is expressed as the function type
    1.20 -%\[ [\tau@1, \ldots, \tau@n]\To \tau. \]
    1.21 -%Finally, the template
    1.22 -%\[ w@0  \;_\; w@1 \;_\; \ldots \;_\; w@n \]
    1.23 -%describes the strings of terminals.
    1.24 -
    1.25 -
    1.26  \subsection{The general mixfix form}
    1.27  Here is a detailed account of mixfix declarations.  Suppose the following
    1.28  line occurs within a {\tt consts} or {\tt syntax} section of a {\tt .thy}
    1.29 @@ -627,7 +608,7 @@
    1.30  $(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where
    1.31  $x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
    1.32  and the whole term has type~$\tau@3$. The optional integer $pb$
    1.33 -specifies the body's priority which defaults to 0.  Special characters
    1.34 +specifies the body's priority, by default~$p$.  Special characters
    1.35  in $\Q$ must be escaped using a single quote.
    1.36  
    1.37  The declaration is expanded internally to something like