diff -r 7b3dd407f6b3 -r 51bc795b81fd Paper/document/root.tex
--- a/Paper/document/root.tex	Sun Mar 28 22:54:38 2010 +0200
+++ b/Paper/document/root.tex	Mon Mar 29 00:30:20 2010 +0200
@@ -9,6 +9,7 @@
 \usepackage{pdfsetup}
 \usepackage{ot1patch}
 \usepackage{times}
+\usepackage{boxedminipage}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -21,7 +22,7 @@
 \renewcommand{\isasymbullet}{{\raisebox{-0.4mm}{\Large$\boldsymbol{\cdot}$}}}
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
 \renewcommand{\isasymequiv}{$\dn$}
-\renewcommand{\isasymiota}{}
+%%\renewcommand{\isasymiota}{}
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \newcommand{\isasymnotapprox}{$\not\approx$}
 \newcommand{\isasymLET}{$\mathtt{let}$}
@@ -31,6 +32,8 @@
 \newcommand{\isasymBIND}{$\mathtt{bind}$}
 \newcommand{\isasymANIL}{$\mathtt{anil}$}
 \newcommand{\isasymACONS}{$\mathtt{acons}$}
+\newcommand{\isasymCASE}{$\mathtt{case}$}
+\newcommand{\isasymOF}{$\mathtt{of}$}
 \newcommand{\LET}{\;\mathtt{let}\;}
 \newcommand{\IN}{\;\mathtt{in}\;}
 \newcommand{\END}{\;\mathtt{end}\;}
@@ -69,7 +72,7 @@
 poorly supported with single binders, such as lambda-abstractions. Our
 extension includes novel definitions of alpha-equivalence and establishes
 automatically the reasoning infrastructure for alpha-equated terms. We
-also provide strong induction principles that have the usual variable
+also prove strong induction principles that have the usual variable
 convention already built in.
 \end{abstract}