--- a/Quotient-Paper/Paper.thy	Mon Jun 07 11:33:00 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Mon Jun 07 15:13:39 2010 +0200
@@ -50,31 +50,33 @@
   \end{flushright}\smallskip
 
   \noindent
-  Isabelle is a generic theorem prover in which many logics can be implemented. 
-  The most widely used one, however, is
-  Higher-Order Logic (HOL). This logic consists of a small number of 
-  axioms and inference
-  rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted 
-  mechanisms for extending the logic: one is the definition of new constants
-  in terms of existing ones; the other is the introduction of new types
-  by identifying non-empty subsets in existing types. It is well understood 
-  to use both mechanisms for dealing with quotient constructions in HOL (see for example 
-  \cite{Paulson06}).
-  For example the integers in Isabelle/HOL are constructed by a quotient construction over 
-  the type @{typ "nat \<times> nat"} and the equivalence relation
+  Isabelle is a generic theorem prover in which many logics can be
+  implemented. The most widely used one, however, is Higher-Order Logic
+  (HOL). This logic consists of a small number of axioms and inference rules
+  over a simply-typed term-language. Safe reasoning in HOL is ensured by two
+  very restricted mechanisms for extending the logic: one is the definition of
+  new constants in terms of existing ones; the other is the introduction of
+  new types by identifying non-empty subsets in existing types. It is well
+  understood to use both mechanisms for dealing with quotient constructions in
+  HOL (see for example \cite{Homeier05,Paulson06}).  For example the integers
+  in Isabelle/HOL are constructed by a quotient construction over the type
+  @{typ "nat \<times> nat"} and the equivalence relation
 
-% I would avoid substraction for natural numbers.
-
-  @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
+  @{text [display, indent=10] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 + n\<^isub>2 = m\<^isub>1 + m\<^isub>2"}
 
   \noindent
-  Similarly one can construct the type of finite sets by quotienting lists
-  according to the equivalence relation
+  This produces the type @{typ int} and definitions for @{text "0::int"} and
+  @{text "1::int"} in terms of pairs of natural numbers can be given (namely
+  @{text "(0, 0)"} and @{text "(1, 0)"}). Operations such as @{text "add::int
+  \<Rightarrow> int \<Rightarrow> int"} can be defined in terms of operations on pairs of natural
+  numbers.  Similarly one can construct the type of finite sets by quotienting
+  lists according to the equivalence relation
 
-  @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
+  @{text [display, indent=10] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
 
   \noindent
-  where @{text "\<in>"} stands for membership in a list.
+  which means two lists are equivalent if every element in one list is also
+  member in the other (@{text "\<in>"} stands here for membership in lists).
 
   The problem is that in order to start reasoning about, for example integers, 
   definitions and theorems need to be transferred, or \emph{lifted}, 

--- a/Quotient-Paper/document/root.tex	Mon Jun 07 11:33:00 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Mon Jun 07 15:13:39 2010 +0200
@@ -24,18 +24,19 @@
 \maketitle
 
 \begin{abstract}
-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 
+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. 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.
+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 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.
 \end{abstract}
 
 % generated text of all theories