--- a/Paper/document/root.tex	Fri Mar 26 16:20:39 2010 +0100
+++ b/Paper/document/root.tex	Fri Mar 26 16:46:40 2010 +0100
@@ -23,6 +23,14 @@
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymiota}{}
 \renewcommand{\isasymemptyset}{$\varnothing$}
+\newcommand{\isasymnotapprox}{$\not\approx$}
+\newcommand{\isasymLET}{$\mathtt{let}$}
+\newcommand{\isasymAND}{$\mathtt{and}$}
+\newcommand{\isasymIN}{$\mathtt{in}$}
+\newcommand{\isasymEND}{$\mathtt{end}$}
+\newcommand{\isasymBIND}{$\mathtt{bind}$}
+\newcommand{\isasymANIL}{$\mathtt{anil}$}
+\newcommand{\isasymACONS}{$\mathtt{acons}$}
 \newcommand{\LET}{\;\mathtt{let}\;}
 \newcommand{\IN}{\;\mathtt{in}\;}
 \newcommand{\END}{\;\mathtt{end}\;}
@@ -56,8 +64,8 @@
 programming language calculi involving named bound variables (as
 opposed to de-Bruijn indices). In this paper we present an extension of
 Nominal Isabelle for dealing with general bindings, that means
-term-constructors where multiple variables are bound at once. Such binding
-structures are ubiquitous in programming language research and only very
+term-constructors where multiple variables are bound at once. Such general
+bindings are ubiquitous in programming language research and only very
 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