diff -r e33e37fd4c7d -r ac69ed8303cc Paper/document/root.tex
--- a/Paper/document/root.tex	Tue Mar 23 09:05:23 2010 +0100
+++ b/Paper/document/root.tex	Tue Mar 23 10:24:12 2010 +0100
@@ -8,6 +8,7 @@
 \usepackage{pgf}
 \usepackage{pdfsetup}
 \usepackage{ot1patch}
+\usepackage{times}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -50,7 +51,7 @@
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
 prover. It provides a proving infrastructure for convenient reasoning about
-programming language calculi involving bound variables that have names (as
+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