--- a/Quotient-Paper-jv/Paper.thy	Wed Dec 21 17:05:00 2011 +0900
+++ b/Quotient-Paper-jv/Paper.thy	Thu Dec 22 04:46:37 2011 +0000
@@ -165,6 +165,9 @@
   makes the formal
   proof of the substitution lemma almost trivial.
 
+  {\bf MAYBE AN EAMPLE FOR PARTIAL QUOTIENTS?}
+
+
   The difficulty is that in order to be able to reason about integers, finite
   sets or $\alpha$-equated lambda-terms one needs to establish a reasoning
   infrastructure by transferring, or \emph{lifting}, definitions and theorems
@@ -331,7 +334,7 @@
   package works in practise.
 *}
 
-section {* Preliminaries and General\\ Quotients\label{sec:prelims} *}
+section {* Preliminaries and General Quotients\label{sec:prelims} *}
 
 text {*
   \noindent
@@ -498,7 +501,7 @@
   \end{isabelle}
 *}
 
-section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
+section {* Quotient Types and Quotient Definitions\label{sec:type} *}
 
 text {*
   \noindent
@@ -758,7 +761,7 @@
   \end{proof}
 *}
 
-section {* Respectfulness and\\ Preservation \label{sec:resp} *}
+section {* Respectfulness and Preservation \label{sec:resp} *}
 
 text {*
   \noindent