--- a/Quotient-Paper/document/root.tex	Mon Jun 21 06:46:28 2010 +0100
+++ b/Quotient-Paper/document/root.tex	Mon Jun 21 06:47:40 2010 +0100
@@ -6,15 +6,31 @@
 \usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{pdfsetup}
-
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{verbdef}
+\usepackage{longtable}
+\usepackage{mathpartir}
 
 \urlstyle{rm}
 \isabellestyle{it}
 \renewcommand{\isastyle}{\isastyleminor}
 
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\verbdef\singlearr|--->|
+\verbdef\doublearr|===>|
+\verbdef\tripple|###|
+
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymUnion}{$\bigcup$}
+
+\newcommand{\isasymsinglearr}{\singlearr}
+\newcommand{\isasymdoublearr}{\doublearr}
+\newcommand{\isasymtripple}{\tripple}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
 
 \begin{document}
 
@@ -24,19 +40,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. We also
+designed our quotient package so that every step in a quotient construction
+can be performed separately and as a result we are 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