# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1279602856 -3600
# Node ID 273f57049bd191929a058c86e60a47c221b00deb
# Parent  44a5388d1d309fe51697db279914cfa3f67ea7dc# Parent  e163fd99de442692c6e74b2976f7759922e10ee5
merged

diff -r e163fd99de44 -r 273f57049bd1 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jul 19 16:59:43 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Tue Jul 20 06:14:16 2010 +0100
@@ -897,8 +897,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
@@ -934,7 +933,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 
@@ -1003,13 +1002,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 *)