--- a/Quotient-Paper/document/root.tex	Thu Jun 10 13:37:32 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Fri Jun 11 14:04:58 2010 +0200
@@ -6,7 +6,8 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{pdfsetup}
-
+\usepackage{tikz}
+\usepackage{pgf}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -24,19 +25,18 @@
 \maketitle
 
 \begin{abstract}
-Higher-order logic (HOL), used in a number of theorem provers, is based on a small
-logic kernel, whose only mechanism for extension is the introduction of safe
-definitions and non-empty types. Both extensions are often performed by
-quotient constructions; for example finite sets are constructed by quotienting
-lists, or integers by quotienting pairs of natural numbers. To ease the work
-involved with quotient constructions, we re-implemented in Isabelle/HOL the
-quotient package by Homeier. In doing so we extended his work in order to deal
-with compositions of quotients. Also, we designed our quotient package so that
-every step in a quotient construction can be performed separately and as a
-result we were able to specify completely the procedure of lifting theorems from
-the raw level to the quotient level.  The importance to programming language
-research is that many properties of programming languages are more convenient
-to verify over $\alpha$-quotient terms, than over raw terms.
+Higher-Order Logic (HOL) is based on a small logic kernel, whose only
+mechanism for extension is the introduction of safe definitions and of
+non-empty types. Both extensions are often performed in quotient
+constructions. To ease the work involved with such quotient constructions, we
+re-implemented in Isabelle/HOL the quotient package by Homeier. In doing so we
+extended his work in order to deal with compositions of quotients. Also, we
+designed our quotient package so that every step in a quotient construction
+can be performed separately and as a result we were able to specify completely
+the procedure of lifting theorems from the raw level to the quotient level.
+The importance for programming language research is that many properties of
+programming language calculi are easier to verify over $\alpha$-equated, or
+$\alpha$-quotient, terms, than over ``raw'' terms.
 \end{abstract}
 
 % generated text of all theories