# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1287073926 -3600
# Node ID 40187684fc160bda95f08ddb0500ba50f8c7ca8c
# Parent  8dbe09606c66e3e4413daf9bfdbe287f4fd84c2a
fixed the typo in the abstract and the problem with append (the type of map_k
and map_list  seems to be indeed incorrect....did not yet look at this)

diff -r 8dbe09606c66 -r 40187684fc16 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu Oct 14 15:58:34 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Thu Oct 14 17:32:06 2010 +0100
@@ -234,7 +234,8 @@
   \end{isabelle}
 
   \noindent
-  We expect that the corresponding operator on finite sets, written @{term "fconcat"},
+  where @{text "@"} is the usual list append. We expect that the corresponding 
+  operator on finite sets, written @{term "fconcat"},
   builds finite unions of finite sets:
 
   \begin{isabelle}\ \ \ \ \ %%%
diff -r 8dbe09606c66 -r 40187684fc16 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Thu Oct 14 15:58:34 2010 +0100
+++ b/Quotient-Paper/document/root.tex	Thu Oct 14 17:32:06 2010 +0100
@@ -69,7 +69,7 @@
 compositions of quotients and also specified completely the procedure 
 of lifting theorems from the raw level to the quotient level.
 The importance for theorem proving is that many formal
-verifications, in order to be feasible, require a convenient resoning infrastructure 
+verifications, in order to be feasible, require a convenient reasoning infrastructure 
 for quotient constructions.
 \end{abstract}