--- a/Quotient-Paper-jv/document/root.tex	Fri Mar 30 16:08:00 2012 +0200
+++ b/Quotient-Paper-jv/document/root.tex	Tue Apr 03 23:09:13 2012 +0100
@@ -9,9 +9,6 @@
 \usepackage{pdfsetup}
 \usepackage{times}
 \usepackage{stmaryrd}
-%\newtheorem{definition}{Definition}
-%\newtheorem{proposition}{Proposition}
-%\newtheorem{lemma}{Lemma}
 
 \urlstyle{rm}
 \isabellestyle{it}
@@ -25,7 +22,6 @@
 
 \renewcommand{\isasymequiv}{$\triangleq$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
-%%\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
 \renewcommand{\isasymUnion}{$\bigcup$}
 \renewcommand{\isacharunderscore}{\text{$\_\!\_$}}
 
@@ -40,7 +36,7 @@
 \title{Quotients Revisited for Isabelle/HOL}
 \author{Cezary Kaliszyk \and Christian Urban}
 \institute{C.~Kaliszyk \at University of Innsbruck, Austria
-     \and C.~Urban \at King's College London, UK}
+      \and C.~Urban \at King's College London, UK}
 \date{Received: date / Accepted: date}
 
 \maketitle
@@ -49,15 +45,14 @@
 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 the %popular
-Isabelle/HOL theorem prover the quotient
-package by Homeier. In doing so we extended his work in order to deal with
-compositions of quotients and also specified completely the procedure
-of lifting theorems from the raw level to the quotient level.
-The importance for theorem proving is that many formal
-verifications, in order to be feasible, require a convenient reasoning infrastructure
-for quotient constructions.
+constructions. To ease the work involved with such quotient
+constructions, we re-implemented in the Isabelle/HOL theorem prover
+the quotient package by Homeier. In doing so we extended his work in
+order to deal with compositions of quotients and also specified
+completely the procedure of lifting theorems from the raw level to the
+quotient level.  The importance for theorem proving is that many
+formal verifications, in order to be feasible, require a convenient
+reasoning infrastructure for quotient constructions.
 \end{abstract}
 
 %\keywords{Quotients, Isabelle theorem prover, Higher-Order Logic}