# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1328283378 -3600
# Node ID 3748acdef916602bb1aa7ccd771a66b6169ec776
# Parent  a9a4baa7779f2b79a3c7e303b6b202e0ecc3b04a
Use the theorem by Brian, requires new Isabelle.

diff -r a9a4baa7779f -r 3748acdef916 Quotient-Paper-jv/Paper.thy
--- a/Quotient-Paper-jv/Paper.thy	Tue Jan 31 16:26:36 2012 +0000
+++ b/Quotient-Paper-jv/Paper.thy	Fri Feb 03 16:36:18 2012 +0100
@@ -325,7 +325,7 @@
   of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation}
   from Homeier \cite{Homeier05}.
 
-  {\bf EXAMPLE BY HUFFMAN ABOUT @{thm map_concat}}
+  {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset[no_vars]}}
 
   In addition we are able to clearly specify what is involved
   in the lifting process (this was only hinted at in \cite{Homeier05} and