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