diff -r 11133eb76f61 -r 93a73eabbffc Paper/document/root.tex --- a/Paper/document/root.tex Tue Sep 28 05:56:11 2010 -0400 +++ b/Paper/document/root.tex Tue Sep 28 08:21:47 2010 -0400 @@ -67,7 +67,8 @@ \maketitle \begin{abstract} -Nominal Isabelle is a definitional extension of the poular Isabelle/HOL theorem +Nominal Isabelle is a definitional extension of the popular 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