525   The syntax of a specification for a term-calculus in Nominal Isabelle is

   525   The syntax of a specification for a term-calculus in Nominal Isabelle is

   526   heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a

   526   heavily inspired by the syntax of the Ott-tool \cite{ott-jfp}. It is a

   527   collection of (possibly mutual recursive) type declarations, say

   527   collection of (possibly mutual recursive) type declarations, say

   528   $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a

   528   $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a

   529   collection of associated binding function declarations, say

   529   collection of associated binding function declarations, say

   531 

   532 

   532   \begin{center}

   533   \begin{center}

   533   \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}

   534   \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}

   534   types \mbox{declaration part} &

   535   types \mbox{declaration part} &

   535   $\begin{cases}

   536   $\begin{cases}