1.1 --- a/doc-src/Ref/theories.tex	Thu Nov 25 11:39:45 1993 +0100
     1.2 +++ b/doc-src/Ref/theories.tex	Thu Nov 25 11:49:21 1993 +0100
     1.3 @@ -1,4 +1,5 @@
     1.4  %% $Id$
     1.5 +
     1.6  \chapter{Theories, Terms and Types} \label{theories}
     1.7  \index{theories|(}\index{signatures|bold}
     1.8  \index{reading!axioms|see{{\tt extend_theory} and {\tt assume_ax}}}
     1.9 @@ -47,7 +48,7 @@
    1.10  $theoryDef$ &=& $id$ {\tt=} $name@1$ {\tt+} \dots {\tt+} $name@n$
    1.11                              [{\tt+} $extension$]\\\\
    1.12  $extension$ &=& [$classes$] [$default$] [$types$] [$arities$] [$consts$]
    1.13 -                [$rules$] {\tt end} [$ml$]\\\\
    1.14 +                [$trans$] [$rules$] {\tt end} [$ml$]\\\\
    1.15  $classes$ &=& \ttindex{classes} $class$ \dots $class$ \\\\
    1.16  $class$ &=& $id$ [{\tt<} $id@1${\tt,} \dots{\tt,} $id@n$] \\\\
    1.17  $default$ &=& \ttindex{default} $sort$ \\\\
    1.18 @@ -67,6 +68,9 @@
    1.19               [ [\quad{\tt[} $k@1${\tt,} \dots{\tt,} $k@n$ {\tt]}\quad] $k$]\\
    1.20         &$|$& $infix$ \\
    1.21         &$|$& \ttindex{binder} $string$ $k$\\\\
    1.22 +$trans$ &=& \ttindex{translations} $transDecl$ \dots $transDecl$ \\\\
    1.23 +$transDecl$ &=& [ {\tt(}$string${\tt)} ] $string$ 
    1.24 +  [ {\tt=>} $|$ {\tt<=} $|$ {\tt==} ] [ ($string$) ] $string$ \\\\
    1.25  $rules$ &=& \ttindex{rules} $rule$ \dots $rule$ \\\\
    1.26  $rule$ &=& $id$ $string$ \\\\
    1.27  $ml$ &=& \ttindex{ML} $text$
    1.28 @@ -123,13 +127,47 @@
    1.29    A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
    1.30      binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
    1.31    like $f(F)$; $p$ is the precedence of the construct.
    1.32 +\item[$transDecl$] Specifies a syntactic translation rule, that is a parse 
    1.33 +  rule ({\tt =>}), a print rule ({\tt <=}), or both ({\tt ==}).
    1.34  \item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
    1.35    names must be distinct.
    1.36  \item[$ml$] This final part of a theory consists of ML code, 
    1.37    typically for parse and print translations.
    1.38  \end{description}
    1.39 -The $mixfix$ and $ml$ sections are explained in more detail in the {\it
    1.40 -Defining Logics} chapter of the {\it Logics} manual.
    1.41 +The $mixfix$, $transDecl$ and $ml$ sections are explained in more detail in 
    1.42 +the {\it Defining Logics} chapter of the {\it Logics} manual.
    1.43 +
    1.44 +
    1.45 +\subsection{Classes and types}
    1.46 +\index{*arities!context conditions}
    1.47 +
    1.48 +Type declarations are subject to the following two well-formedness
    1.49 +conditions:
    1.50 +\begin{itemize}
    1.51 +\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
    1.52 +  with $\vec{r} \neq \vec{s}$.  For example
    1.53 +\begin{ttbox}
    1.54 +types ty 1
    1.55 +arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic
    1.56 +        ty :: ({\ttlbrace}{\ttrbrace})logic
    1.57 +\end{ttbox}
    1.58 +leads to an error message and fails.
    1.59 +\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
    1.60 +  (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
    1.61 +  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
    1.62 +\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
    1.63 +expresses that the set of types represented by $s'$ is a subset of the set of
    1.64 +types represented by $s$.  For example
    1.65 +\begin{ttbox}
    1.66 +classes term < logic
    1.67 +types ty 1
    1.68 +arities ty :: ({\ttlbrace}logic{\ttrbrace})logic
    1.69 +        ty :: ({\ttlbrace}{\ttrbrace})term
    1.70 +\end{ttbox}
    1.71 +leads to an error message and fails.
    1.72 +\end{itemize}
    1.73 +These conditions guarantee principal types~\cite{nipkow-prehofer}.
    1.74 +
    1.75  
    1.76  \section{Loading Theories}
    1.77  \label{LoadingTheories}