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