diff -r 883b38196dba -r a9cb6a51efc3 Paper/document/root.tex
--- a/Paper/document/root.tex	Thu Mar 18 11:36:03 2010 +0100
+++ b/Paper/document/root.tex	Thu Mar 18 11:37:10 2010 +0100
@@ -3,11 +3,10 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{pdfsetup}
 
-%\ConferenceShortName{ICFP}
-%\ConferenceName{International Conference on Functional Programming}
-
-\usepackage{pdfsetup}
 \urlstyle{rm}
 \isabellestyle{it}
 
@@ -19,10 +18,9 @@
 \renewcommand{\isasymemptyset}{$\varnothing$}
 
 
-% for uniform font size
-%\renewcommand{\isastyle}{\isastyleminor}
 
 %----------------- theorem definitions ----------
+\newtheorem{Property}{Theorem}[section]
 \newtheorem{Theorem}{Theorem}[section]
 \newtheorem{Definition}[Theorem]{Definition}
 \newtheorem{Example}{\it Example}[section]
@@ -41,18 +39,18 @@
 \maketitle
 \begin{abstract} 
 Nominal Isabelle is a definitional extension of the Isabelle/HOL
-theorem prover. It provides a reasoning infrastructure for formalisations
-of programming language calculi. In this paper we present an extension
-of Nominal Isabelle with general binding constructs. Such constructs
-are important in formalisation ...
+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.
 \end{abstract}
 
-%\begin{keywords}
-%Language formalisations, Isabelle/HOL, POPLmark
-%\end{keywords}
 
-
-% generated text of all theories
 \input{session}
 
 \bibliographystyle{plain}