2124   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 

  2124   meaning in a HOL-based theorem prover. We also had to generalise slightly Ott's 

  2125   binding clauses. In Ott you specify binding clauses with a single body; we 

  2125   binding clauses. In Ott you specify binding clauses with a single body; we 

  2126   allow more than one. We have to do this, because this makes a difference 

  2126   allow more than one. We have to do this, because this makes a difference 

  2127   for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and 

  2127   for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and 

  2128   \isacommand{bind (res)}. 

  2128   \isacommand{bind (res)}. 

  2130   %Consider the examples

  2130   %Consider the examples

  2131   %

  2131   %

  2132   %\begin{center}

  2132   %\begin{center}

  2133   %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  2133   %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}

  2134   %@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  

  2134   %@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  

  2151   %@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\

  2151   %@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\

  2152   %@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 

  2152   %@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 

  2153   %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\

  2153   %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\

  2154   %\end{tabular}

  2154   %\end{tabular}

  2155   %\end{center}

  2155   %\end{center}

  2158   %and therefore need the extra generality to be able to distinguish between 

  2158   %and therefore need the extra generality to be able to distinguish between 

  2159   %both specifications.

  2159   %both specifications.

  2160   Because of how we set up our definitions, we also had to impose some restrictions

  2160   Because of how we set up our definitions, we also had to impose some restrictions

  2161   (like a single binding function for a deep binder) that are not present in Ott. Our

  2161   (like a single binding function for a deep binder) that are not present in Ott. Our

  2162   expectation is that we can still cover many interesting term-calculi from

  2162   expectation is that we can still cover many interesting term-calculi from