1.1 --- a/doc-src/Intro/advanced.tex	Thu Mar 24 17:54:32 1994 +0100
     1.2 +++ b/doc-src/Intro/advanced.tex	Thu Mar 24 18:00:11 1994 +0100
     1.3 @@ -352,6 +352,8 @@
     1.4  rules on abstract syntax trees, for defining notations and abbreviations.
     1.5  The {\ML} section contains code to perform arbitrary syntactic
     1.6  transformations.  The main declaration forms are discussed below.
     1.7 +The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
     1.8 +  appendix of the {\it Reference Manual}}{Appendix~\ref{app:TheorySyntax}}.
     1.9  
    1.10  All the declaration parts can be omitted.  In the simplest case, $T$ is
    1.11  just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
    1.12 @@ -432,7 +434,7 @@
    1.13  
    1.14  
    1.15  \subsection{Declaring type constructors}
    1.16 -\indexbold{types!declaring}\indexbold{arities!declaring} 
    1.17 +\indexbold{types!declaring}\indexbold{arities!declaring}
    1.18  %
    1.19  Types are composed of type variables and {\bf type constructors}.  Each
    1.20  type constructor takes a fixed number of arguments.  They are declared
    1.21 @@ -516,6 +518,34 @@
    1.22  translator passes them verbatim to the {\ML} output file.
    1.23  \end{warn}
    1.24  
    1.25 +\subsection{Type synonyms}
    1.26 +\indexbold{types!synonyms}\index{types!abbreviations|see{synonyms}}
    1.27 +
    1.28 +Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
    1.29 +to those found in ML. Such synonyms are defined in the type declaration part
    1.30 +and are fairly self explanatory:
    1.31 +\begin{ttbox}
    1.32 +types gate = "[o,o] => o"
    1.33 +      'a pred = "'a => o"
    1.34 +      ('a,'b)nuf = "'b => 'a"
    1.35 +\end{ttbox}
    1.36 +Type declarations and synonyms can be mixed arbitrarily:
    1.37 +\begin{ttbox}
    1.38 +types nat
    1.39 +      'a stream = "nat => 'a"
    1.40 +      signal = "nat stream"
    1.41 +      'a list
    1.42 +\end{ttbox}
    1.43 +A synonym is merely an abbreviation for some existing type expression. Hence
    1.44 +synonyms may not be recursive! Internally all synonyms are fully expanded. As
    1.45 +a consequence Isabelle output never contains synonyms. Their main purpose is
    1.46 +to improve the readability of theories. Synonyms can be used just like any
    1.47 +other type:
    1.48 +\begin{ttbox}
    1.49 +consts and,or :: "gate"
    1.50 +       negate :: "signal => signal"
    1.51 +\end{ttbox}
    1.52 +
    1.53  \subsection{Infixes and Mixfixes}
    1.54  \indexbold{infix operators}\index{examples!of theories}
    1.55  The constant declaration part of the theory