--- a/Paper/document/root.tex	Thu Mar 18 15:32:49 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 16:22:10 2010 +0100
@@ -20,7 +20,7 @@
 
 
 %----------------- theorem definitions ----------
-\newtheorem{Property}{Theorem}[section]
+\newtheorem{property}{Property}[section]
 \newtheorem{Theorem}{Theorem}[section]
 \newtheorem{Definition}[Theorem]{Definition}
 \newtheorem{Example}{\it Example}[section]
@@ -38,16 +38,15 @@
 
 \maketitle
 \begin{abstract} 
-Nominal Isabelle is a definitional extension of the Isabelle/HOL
-theorem prover. It provides a proving infrastructure for
-conveninet reasoning about programming language calculi. In this paper 
-we present an extension of Nominal Isabelle for dealing with general binding 
-structures. Such structures are ubiquitous in programming language research
-and only very poorly handled by the well-known single abstraction in the
-lambda-calculus. We give definitions for alpha-equivalence and establish
-the reasoning structure for alpha-equated terms. For example we provide
-a strong induction principle that has the variable convention already
-built in.
+Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
+prover. It provides a proving infrastructure for convenient reasoning about
+programming language calculi. In this paper we present an extension of Nominal
+Isabelle for dealing with general binding structures. Such binding structures are
+ubiquitous in programming language research and only very poorly handled by
+single binding from the lambda-calculus. We give in this
+paper novel definitions for alpha-equivalence and establish automatically the
+reasoning structure for alpha-equated terms. For example we provide a strong
+induction principle that has the variable convention already built in.
 \end{abstract}