diff -r 231a20534950 -r 02e03d4287ec Quotient-Paper/Paper.thy
--- 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},