--- a/Paper/document/root.tex	Thu Mar 18 16:22:10 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 18:43:03 2010 +0100
@@ -16,6 +16,10 @@
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymiota}{}
 \renewcommand{\isasymemptyset}{$\varnothing$}
+\newcommand{\LET}{\;\mathtt{let}\;}
+\newcommand{\IN}{\;\mathtt{in}\;}
+\newcommand{\END}{\;\mathtt{end}\;}
+\newcommand{\AND}{\;\mathtt{and}\;}
 
 
 
@@ -41,12 +45,13 @@
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
 programming language calculi. In this paper we present an extension of Nominal
-Isabelle for dealing with general binding structures. Such binding structures are
-ubiquitous in programming language research and only very poorly handled by
-single binding from the lambda-calculus. We give in this
-paper novel definitions for alpha-equivalence and establish automatically the
-reasoning structure for alpha-equated terms. For example we provide a strong
-induction principle that has the variable convention already built in.
+Isabelle for dealing with general binding structures. Such binding structures
+are ubiquitous in programming language research and only very poorly supported
+by theorem provers providing only single binding as in the lambda-calculus. We
+give in this paper novel definitions for alpha-equivalence and establish
+automatically the reasoning structure for alpha-equated terms. For example we
+provide a strong induction principle that has the variable convention already
+built in.
 \end{abstract}