# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1286349189 -3600
# Node ID ae860c95bf9f32977ed613d3d19fe233c88ac899
# Parent  b5cb3183409e9e8d044bd91d3f85599b71bf4b82
tuned

diff -r b5cb3183409e -r ae860c95bf9f Paper/Paper.thy
--- a/Paper/Paper.thy	Wed Oct 06 08:09:40 2010 +0100
+++ b/Paper/Paper.thy	Wed Oct 06 08:13:09 2010 +0100
@@ -2126,7 +2126,7 @@
   allow more than one. We have to do this, because this makes a difference 
   for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and 
   \isacommand{bind (res)}. 
-
+  %
   %Consider the examples
   %
   %\begin{center}
@@ -2153,8 +2153,8 @@
   %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
   %\end{tabular}
   %\end{center}
-
-  \noindent
+  %
+  %\noindent
   %and therefore need the extra generality to be able to distinguish between 
   %both specifications.
   Because of how we set up our definitions, we also had to impose some restrictions