--- a/Paper/Paper.thy	Tue Mar 23 10:26:46 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 11:52:55 2010 +0100
@@ -522,27 +522,77 @@
 section {* Alpha-Equivalence and Free Variables *}
 
 text {*
-  A specification of a term-calculus in Nominal Isabelle is a collection
-  of (possibly mutual recursive) type declarations, say $ty_1$, $ty_2$, \ldots $ty_n$ 
-  written as follows:
+  The syntax of a specification for a term-calculus in Nominal Isabelle is
+  heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a
+  collection of (possibly mutual recursive) type declarations, say
+  $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a
+  collection of associated binding function declarations, say
+  $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are written as follows:
 
   \begin{center}
-  \begin{tabular}{l}
-  \isacommand{nominal\_datatype} $ty_{\alpha{}1} =$\\
-  \isacommand{and} $ty_{\alpha{}2} =$\\
+  \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}
+  types \mbox{declaration part} &
+  $\begin{cases}
+  \mbox{\begin{tabular}{l}
+  \isacommand{nominal\_datatype} $ty_{\alpha{}1} = \ldots$\\
+  \isacommand{and} $ty_{\alpha{}2} = \ldots$\\
   $\ldots$\\ 
-  \isacommand{and} $ty_{\alpha{}}n =$\\ 
+  \isacommand{and} $ty_{\alpha{}n} = \ldots$\\ 
+  \end{tabular}}
+  \end{cases}$\\
+  binding \mbox{functions part} &
+  $\begin{cases}
+  \mbox{\begin{tabular}{l}
+  \isacommand{with} $bn_{\alpha{}1}$ \isacommand{and} \ldots \isacommand{and} $bn_{\alpha{}m}$
   $\ldots$\\
-  \isacommand{with}\\
+  \isacommand{where}\\
   $\ldots$\\
+  \end{tabular}}
+  \end{cases}$\\
   \end{tabular}
   \end{center}
 
   \noindent
-  The section below the \isacommand{with} are binding functions, which
-  will be explained below.
+  Each type declaration $ty_{\alpha{}i}$ consists of a collection of 
+  term-constructors, each of which comes with a list of labelled 
+  types that indicate the types of the arguments of the term-constructor,
+  like 
+
+  \begin{center}
+  $C_\alpha\;label_1\!::\!ty'_1\;\ldots label_j\!::\!ty'_j\;\;\textit{binding\_clauses}$ 
+  \end{center}
   
+  \noindent
+  The labels are optional and can be used in the (possibly empty) list of binding clauses.
+  These clauses indicate the binders and the scope of the binders in a term-constructor. They
+  are of the form
 
+  \begin{center}
+  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it label} 
+  \end{center}
+
+  \noindent
+  whereby we distinguish between \emph{shallow} binders and \emph{deep} binders.
+  Shallow binders are just of the form \isacommand{bind}\; {\it label}\; 
+  \isacommand{in}\; {\it another\_label}. The only restriction on shallow binders
+  is that the {\it label} must refer to either a type which is single atom or
+  to a type which is a finite set of atoms. For example the specification of 
+  lambda-terms and type-schemes use them:
+
+  \begin{center}
+  \begin{tabular}{cc}
+  \begin{tabular}{l}
+  \isacommand{nominal\_datatype} lam =\\
+  \hspace{5mm}Var\;{\it name}\\
+  \hspace{5mm}App\;{\it lam}\;{\it lam}\\
+  \hspace{5mm}Lam\;{\it x::name}\;{\it t::lam}\;
+  \isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+  \end{tabular} &
+  \begin{tabular}{l}
+  foo
+  \end{tabular}
+  \end{tabular}
+  \end{center}
 
   A specification of a term-calculus in Nominal Isabell is very similar to 
   the usual datatype definition of Isabelle/HOL: