--- a/doc-src/Codegen/Thy/document/Further.tex Fri Nov 05 15:15:28 2010 -0700
+++ b/doc-src/Codegen/Thy/document/Further.tex Sat Nov 06 10:01:00 2010 -0700
@@ -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%
%