--- a/doc-src/Codegen/Thy/document/Further.tex Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Further.tex Wed Nov 03 14:14:06 2010 +0100
@@ -240,7 +240,8 @@
specific application, you should consider \emph{Imperative
Functional Programming with Isabelle/HOL}
\cite{bulwahn-et-al:2008:imperative}; the framework described there
- is available in session \isa{Imperative{\isacharunderscore}HOL}.%
+ is available in session \isa{Imperative{\isacharunderscore}HOL}, together with a short
+ primer document.%
\end{isamarkuptext}%
\isamarkuptrue%
%