# HG changeset patch
# User nipkow
# Date 764528411 -3600
# Node ID 0746399cfd4436f3b86c2615b8f8fb70e68eebaa
# Parent  7e2cffe28eb5f8043ba844d9af29dafedb3aa680
added section on type synonyms

diff -r 7e2cffe28eb5 -r 0746399cfd44 doc-src/Intro/advanced.tex
--- a/doc-src/Intro/advanced.tex	Thu Mar 24 17:54:32 1994 +0100
+++ b/doc-src/Intro/advanced.tex	Thu Mar 24 18:00:11 1994 +0100
@@ -352,6 +352,8 @@
 rules on abstract syntax trees, for defining notations and abbreviations.
 The {\ML} section contains code to perform arbitrary syntactic
 transformations.  The main declaration forms are discussed below.
+The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
+  appendix of the {\it Reference Manual}}{Appendix~\ref{app:TheorySyntax}}.
 
 All the declaration parts can be omitted.  In the simplest case, $T$ is
 just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
@@ -432,7 +434,7 @@
 
 
 \subsection{Declaring type constructors}
-\indexbold{types!declaring}\indexbold{arities!declaring} 
+\indexbold{types!declaring}\indexbold{arities!declaring}
 %
 Types are composed of type variables and {\bf type constructors}.  Each
 type constructor takes a fixed number of arguments.  They are declared
@@ -516,6 +518,34 @@
 translator passes them verbatim to the {\ML} output file.
 \end{warn}
 
+\subsection{Type synonyms}
+\indexbold{types!synonyms}\index{types!abbreviations|see{synonyms}}
+
+Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
+to those found in ML. Such synonyms are defined in the type declaration part
+and are fairly self explanatory:
+\begin{ttbox}
+types gate = "[o,o] => o"
+      'a pred = "'a => o"
+      ('a,'b)nuf = "'b => 'a"
+\end{ttbox}
+Type declarations and synonyms can be mixed arbitrarily:
+\begin{ttbox}
+types nat
+      'a stream = "nat => 'a"
+      signal = "nat stream"
+      'a list
+\end{ttbox}
+A synonym is merely an abbreviation for some existing type expression. Hence
+synonyms may not be recursive! Internally all synonyms are fully expanded. As
+a consequence Isabelle output never contains synonyms. Their main purpose is
+to improve the readability of theories. Synonyms can be used just like any
+other type:
+\begin{ttbox}
+consts and,or :: "gate"
+       negate :: "signal => signal"
+\end{ttbox}
+
 \subsection{Infixes and Mixfixes}
 \indexbold{infix operators}\index{examples!of theories}
 The constant declaration part of the theory