diff -r 200954544cae -r e08e3c29dbc0 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue May 11 12:18:26 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Tue May 11 14:58:46 2010 +0100
@@ -12,6 +12,9 @@
 section {* Introduction *}
 
 text {* 
+  {\hfill quote by Larry}\bigskip
+
+  \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 
@@ -27,10 +30,40 @@
   @{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"}
 
   \noindent
-  The problem is that one 
+  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)"}
+
+  \noindent
+  where @{text "\<in>"} stands for membership in a list.
+
+  The problem is that in order to start reasoning about, for example integers, 
+  definitions and theorems need to be transferred, or \emph{lifted}, 
+  from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. 
+  This lifting usually requires a lot of tedious reasoning effort.
+  The purpose of a \emph{quotient package} is to ease the lifting and automate
+  the reasoning involved as much as possible. Such a package is a central
+  component of the new version of Nominal Isabelle where representations 
+  of alpha-equated terms are constructed according to specifications given by
+  the user. 
   
+  In the context of HOL, there have been several quotient packages (...). The
+  most notable is the one by Homeier (...) implemented in HOL4. However, what is
+  surprising, none of them can deal compositions of quotients, for example with 
+  lifting theorems about @{text "concat"}:
 
+  @{text [display] "concat definition"}
+  
+  \noindent
+  One would like to lift this definition to the operation
+  
+  @{text [display] "union definition"}
 
+  \noindent
+  What is special about this operation is that we have as input
+  lists of lists which after lifting turn into finite sets of finite
+  sets. 
 *}
 
 subsection {* Contributions *}