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)
--- 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}\ \ \ \ \ %%%
--- 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}