--- a/Quotient-Paper/document/root.tex	Sun Jun 06 13:16:27 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Mon Jun 07 11:33:00 2010 +0200
@@ -12,6 +12,10 @@
 \isabellestyle{it}
 \renewcommand{\isastyle}{\isastyleminor}
 
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+
 \begin{document}
 
 \title{Quotients Revisited for Isabelle/HOL}
@@ -20,16 +24,18 @@
 \maketitle
 
 \begin{abstract}
-Higher-order logic (HOL) is based on a small logic kernel, whose 
-only mechanism for extension is the introduction of definitions 
-and types. Both extensions are often performed by 
-quotient constructions, for example finite sets are constructed by quotienting
+Higher-order logic (HOL), used in several 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. 
+can be performed separately. 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.
 \end{abstract}
 
 % generated text of all theories