equal
deleted
inserted
replaced
323 according to the type of the raw constant and the type |
323 according to the type of the raw constant and the type |
324 of the quotient constant. This means we also have to extend the notions |
324 of the quotient constant. This means we also have to extend the notions |
325 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
325 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
326 from Homeier \cite{Homeier05}. |
326 from Homeier \cite{Homeier05}. |
327 |
327 |
328 {\bf EXAMPLE BY HUFFMAN ABOUT @{thm map_concat}} |
328 {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset[no_vars]}} |
329 |
329 |
330 In addition we are able to clearly specify what is involved |
330 In addition we are able to clearly specify what is involved |
331 in the lifting process (this was only hinted at in \cite{Homeier05} and |
331 in the lifting process (this was only hinted at in \cite{Homeier05} and |
332 implemented as a ``rough recipe'' in ML-code). A pleasing side-result |
332 implemented as a ``rough recipe'' in ML-code). A pleasing side-result |
333 is that our procedure for lifting theorems is completely deterministic |
333 is that our procedure for lifting theorems is completely deterministic |