--- a/Paper/Paper.thy	Thu Mar 18 19:02:33 2010 +0100
+++ b/Paper/Paper.thy	Thu Mar 18 19:39:01 2010 +0100
@@ -133,9 +133,19 @@
   \noindent
   where the $x_i$ are bound in $s$. In this term we might not care about the order in 
   which the $x_i = t_i$ are given, but we do care about the information that there are 
-  as many $x_i$ as there are $t_i$. We lose this information if we represent the $\mathtt{let}$
-  as something 
+  as many $x_i$ as there are $t_i$. We lose this information if we specify the 
+  $\mathtt{let}$-constructor as something like 
+
+  \begin{center}
+  $\LET [x_1,\ldots,x_n].s\; [t_1,\ldots,t_n]$
+  \end{center}
 
+  \noindent
+  where the $[\_].\_$ indicates that a list of variables become bound
+  in $s$. In this representation we need additional predicates to ensure 
+  that the two lists are of equal length. This can result into very 
+  elaborate reasoning (see \cite{BengtsonParow09}). 
+  
   
 
   

--- a/Paper/document/root.tex	Thu Mar 18 19:02:33 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 19:39:01 2010 +0100
@@ -6,10 +6,13 @@
 \usepackage{tikz}
 \usepackage{pgf}
 \usepackage{pdfsetup}
+\usepackage{ot1patch}
 
 \urlstyle{rm}
 \isabellestyle{it}
 
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}