# HG changeset patch # User Christian Urban # Date 1268937541 -3600 # Node ID eb95360d6ac6fae8120af4ee72edede381849910 # Parent 4f8bab472a83e083a3f8ae740d0f31575819d676 another little bit for the introduction diff -r 4f8bab472a83 -r eb95360d6ac6 Paper/Paper.thy --- 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}). + diff -r 4f8bab472a83 -r eb95360d6ac6 Paper/document/root.tex --- 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}}{=}\,}