diff -r fbdaaa20396b -r 1c18f2cf3923 Paper/document/root.tex --- a/Paper/document/root.tex Sat Sep 25 08:38:04 2010 -0400 +++ b/Paper/document/root.tex Sun Sep 26 17:57:30 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