# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1277131319 -3600
# Node ID 7c8783d2dcd0ab9906487840d3ad1ae13399cb49
# Parent  49cc1af89de99394eadc3ea6b936a8245d2bc30f
further post-submission tuning

diff -r 49cc1af89de9 -r 7c8783d2dcd0 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Mon Jun 21 06:47:40 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Mon Jun 21 15:41:59 2010 +0100
@@ -347,8 +347,8 @@
   \end{isabelle}
   
   \noindent
-  In the context of quotients, the following two notions from are \cite{Homeier05} 
-  needed later on.
+  In the context of quotients, the following two notions from \cite{Homeier05} 
+  are needed later on.
 
   \begin{definition}[Respects]\label{def:respects}
   An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
@@ -394,7 +394,8 @@
 
   \begin{definition}[Composition of Relations]
   @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
-  composition defined by @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
+  composition defined by 
+  @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
   holds if and only if @{thm (prem 1) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]} and
   @{thm (prem 2) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}.
   \end{definition}
@@ -410,7 +411,7 @@
   composing @{text "\<approx>\<^bsub>list\<^esub>"} will be necessary: given @{term "Quotient R Abs Rep"} 
   with @{text R} being an equivalence relation, then
 
-  @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep \<circ> rep_fset)"}
+  @{text [display, indent=10] "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map Abs) (map Rep \<circ> Rep_fset)"}
 
   \vspace{-.5mm}
 *}
@@ -838,14 +839,16 @@
   The second and third proof step will always succeed if the appropriate
   respectfulness and preservation theorems are given. In contrast, the first
   proof step can fail: a theorem given by the user does not always
-  imply a regularized version and a stronger one needs to be proved. This
-  is outside of the scope where the quotient package can help. An example
+  imply a regularized version and a stronger one needs to be proved. An example
   for this kind of failure is the simple statement for integers @{text "0 \<noteq> 1"}.
   One might hope that it can be proved by lifting @{text "(0, 0) \<noteq> (1, 0)"},  
-  but the raw theorem only shows that particular element in the
-  equivalence classes are not equal. A more general statement stipulating that
-  the equivalence classes are not equal is necessary, and then leads to the
-  theorem  @{text "0 \<noteq> 1"}.
+  but this raw theorem only shows that particular element in the
+  equivalence classes are not equal. In order to obtain @{text "0 \<noteq> 1"}, a  
+  more general statement stipulating that the equivalence classes are not 
+  equal is necessary.  This kind of failure is beyond the scope where the 
+  quotient package can help: the user has to provide a raw theorem that
+  can be regularized automatically, or has to provide an explicit proof
+  for the first proof step.
 
   In the following we will first define the statement of the
   regularized theorem based on @{text "raw_thm"} and
@@ -923,12 +926,12 @@
   \end{center}
 
   \noindent 
-  where again the cases for existential quantifiers and unique existential
-  quantifiers have been omitted.
+  In this definition we again omitted the cases for existential and unique existential
+  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 
-  the implications into simpler implication subgoals. This succeeds for every
+  the implications into simpler implicational subgoals. This succeeds for every
   monotone connective, except in places where the function @{text REG} inserted,
   for instance, a quantifier by a bounded quantifier. In this case we have 
   rules of the form