--- a/Paper/document/root.tex	Tue Jun 29 18:00:59 2010 +0100
+++ b/Paper/document/root.tex	Wed Jun 30 16:56:37 2010 +0100
@@ -62,11 +62,11 @@
 \title{\LARGE\bf General Bindings and Alpha-Equivalence in Nominal Isabelle}
 \authorinfo{Christian Urban and Cezary Kaliszyk}
            {TU Munich, Germany}
-           {urbanc/kaliszyk@in.tum.de}
+           {\{urbanc, kaliszyk\}@in.tum.de}
 \maketitle
 
 \begin{abstract} 
-Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
+Nominal Isabelle is a definitional extension of the poular Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
 programming language calculi involving named bound variables (as
 opposed to de-Bruijn indices). In this paper we present an extension of
@@ -74,8 +74,8 @@
 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
+extension includes novel definitions of $\alpha$-equivalence and establishes
+automatically the reasoning infrastructure for $\alpha$-equated terms. We
 also prove strong induction principles that have the usual variable
 convention already built in.
 \end{abstract}
@@ -83,10 +83,10 @@
 \category{CR-number}{subcategory}{third-level}
 
 \terms
-term1, term2
+formal reasoning, programming language calculi
 
 \keywords
-keyword1, keyword2
+nominal logic work, variable convention
 
 
 \input{session}