--- a/Paper/document/root.tex	Mon Oct 04 07:25:37 2010 +0100
+++ b/Paper/document/root.tex	Mon Oct 04 12:39:57 2010 +0100
@@ -1,4 +1,5 @@
 \documentclass{llncs}
+\usepackage{times}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{amsmath}
@@ -60,15 +61,14 @@
 
 \begin{document}
 
-\title{General Bindings and Alpha-Equivalence in Nominal Isabelle}
+\title{General Bindings and Alpha-Equivalence\\ in Nominal Isabelle}
 \author{Christian Urban and Cezary Kaliszyk}
 \institute{TU Munich, Germany}
 %%%{\{urbanc, kaliszyk\}@in.tum.de}
 \maketitle
 
 \begin{abstract} 
-Nominal Isabelle is a definitional extension of the popular Isabelle/HOL 
-theorem
+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 named bound variables (as
 opposed to de-Bruijn indices). In this paper we present an extension of