--- a/Quotient-Paper/Paper.thy	Mon Jul 19 08:34:38 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Mon Jul 19 08:55:49 2010 +0100
@@ -893,8 +893,7 @@
   \noindent
   In the above definition we omitted the cases for existential quantifiers
   and unique existential quantifiers, as they are very similar to the cases
-  for the universal quantifier. For the third and fourth clause, note that 
-  @{text "\<forall>x. P"} is defined as @{text "\<forall> (\<lambda>x. P)"}.
+  for the universal quantifier. 
 
   Next we define the function @{text INJ} which takes as argument
   @{text "reg_thm"} and @{text "quot_thm"} (both as
@@ -930,7 +929,7 @@
 
   \noindent 
   In this definition we again omitted the cases for existential and unique existential
-  quantifiers.
+  quantifiers. 
 
   In the first proof step, establishing @{text "raw_thm \<longrightarrow> reg_thm"}, we always 
   start with an implication. Isabelle provides \emph{mono} rules that can split up 
@@ -999,13 +998,14 @@
   Next, relations over lifted types are folded to equalities.
   For this the following theorem has been shown by  Homeier~\cite{Homeier05}:
 
-    @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
+  @{thm [display, indent=10] (concl) Quotient_rel_rep[no_vars]}
 
   \noindent
   Finally, we rewrite with the preservation theorems. This will result
   in two equal terms that can be solved by reflexivity.
   *}
 
+
 section {* Examples \label{sec:examples} *}
 
 (* Mention why equivalence *)