--- a/Quotient-Paper/Paper.thy	Tue Jun 15 09:12:54 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 09:22:38 2010 +0200
@@ -785,10 +785,10 @@
   \begin{tabular}{rcl}
   \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions (with same types and different types):}\\
   @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma>. REG (t, s)"}\\
-  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+  @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s)"} & $\dn$ & @{text "\<lambda>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{quantification (over same types and different types):}\\
   @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma>. REG (t, s)"}\\
-  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
+  @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s)"} & $\dn$ & @{text "\<forall>x : \<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}\\
   \multicolumn{3}{@ {\hspace{-4mm}}l}{equalities (with same types and different types):}\\
   @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>)"} & $\dn$ & @{text "(op =) : \<sigma>"}\\
   @{text "REG ((op =) : \<sigma>, (op =) : \<tau>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>) : \<sigma>"}\\
@@ -1029,27 +1029,8 @@
 
 text {*
 
-  Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
-  defines quotient types for Isabelle/HOL. It did not include theorem lifting.
-  John Harrison's quotient package~\cite{harrison-thesis} is the first one to
-  lift theorems, however only first order. There is work on quotient types in
-  non-HOL based systems and logical frameworks, namely theory interpretations
-  in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
-  the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
-  Larry Paulson shows a construction of quotients that does not require the
-  Hilbert Choice operator, again only first order~\cite{Paulson06}.
-
-  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},
-  which is the first one to support lifting of higher order theorems. In
-  comparison with this package we explore the notion of composition of quotients,
-  which allows lifting constants like @{term "concat"} and theorems about it.
-  The HOL4 package requires a big lists of constants, theorems to lift,
-  respectfullness conditions as input. Our package is modularized, so that
-  single definitions, single theorems or single respectfullness conditions etc
-  can be added, which allows a natural use of the quotient package together
-  with type-classes and locales.
-
-  The code of the quotient package described here is already included in the
+  The code of the quotient package and the examples described here are
+  already included in the
   standard distribution of Isabelle.\footnote{Available from
   \href{http://isabelle.in.tum.de/}{http://isabelle.in.tum.de/}.} It is
   heavily used in Nominal Isabelle, which provides a convenient reasoning
@@ -1060,38 +1041,42 @@
   concurrency \cite{BengtsonParow09} and a strong normalisation result for
   cut-elimination in classical logic \cite{UrbanZhu08}.
 
-*}
+  Oscar Slotosch~\cite{Slotosch97} implemented a mechanism that automatically
+  defines quotient types for Isabelle/HOL. It did not include theorem lifting.
+  John Harrison's quotient package~\cite{harrison-thesis} is the first one to
+  lift theorems, however only first order. There is work on quotient types in
+  non-HOL based systems and logical frameworks, namely theory interpretations
+  in PVS~\cite{PVS:Interpretations}, new types in MetaPRL~\cite{Nogin02}, or
+  the use of setoids in Coq, with some higher order issues~\cite{ChicliPS02}.
+  Larry Paulson shows a construction of quotients that does not require the
+  Hilbert Choice operator, again only first order~\cite{Paulson06}.
+  The closest to our package is the package for HOL4 by Peter Homeier~\cite{Homeier05},
+  which is the first one to support lifting of higher order theorems.
 
 
-subsection {* Contributions *}
-
-text {*
-  We present the detailed lifting procedure, which was not shown before.
-
-  The quotient package presented in this paper has the following
-  advantages over existing packages:
-  \begin{itemize}
-
-  \item We define quotient composition, function map composition and
-    relation map composition. This lets lifting polymorphic types with
-    subtypes quotiented as well. We extend the notions of
-    respectfulness and preservation to cope with quotient
-    composition.
+  Our quotient package for the first time explore the notion of
+  composition of quotients, which allows lifting constants like @{term
+  "concat"} and theorems about it. We defined the composition of
+  relations and showed examples of compositions of quotients which
+  allows lifting polymorphic types with subtypes quotiented as well.
+  We extended the notions of respectfullness and preservation;
+  with quotient compositions there is more than one condition needed
+  for a constant.
 
-  \item We allow lifting only some occurrences of quotiented
-    types. Rsp/Prs extended. (used in nominal)
+  Our package is modularized, so that single definitions, single
+  theorems or single respectfullness conditions etc can be added,
+  which allows the use of the quotient package together with
+  type-classes and locales. This has the advantage over packages
+  requiring big lists as input for the user of being able to develop
+  a theory progressively.
 
-  \item The quotient package is very modular. Definitions can be added
-    separately, rsp and prs can be proved separately, Quotients and maps
-    can be defined separately and theorems can
-    be lifted on a need basis. (useful with type-classes).
-
-  \item Can be used both manually (attribute, separate tactics,
-    rsp/prs databases) and programatically (automated definition of
-    lifted constants, the rsp proof obligations and theorem statement
-    translation according to given quotients).
-
-  \end{itemize}
+  We allow lifting only some occurrences of quotiented types, which
+  is useful in Nominal. The package can be used automatically with
+  an attribute, manually with separate tactics for parts of the lifting
+  procedure, and programatically. Automated definitions of constants
+  and respectfulness proof obligations are used in Nominal. Finally
+  we streamlined and showed the detailed lifting procedure, which
+  has not been presented before.
 
   \medskip
   \noindent