Use the theorem by Brian, requires new Isabelle.
authorCezary Kaliszyk <cezarykaliszyk@gmail.com>
Fri, 03 Feb 2012 16:36:18 +0100
changeset 3115 3748acdef916
parent 3114 a9a4baa7779f
child 3117 bd602eb894ab
Use the theorem by Brian, requires new Isabelle.
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