doc-src/Codegen/Thy/Further.thy
changeset 39064 67f0cb151eb2
parent 38510 ec0408c7328b
child 39559 e7d4923b9b1c
--- a/doc-src/Codegen/Thy/Further.thy	Thu Sep 02 16:41:41 2010 +0200
+++ b/doc-src/Codegen/Thy/Further.thy	Thu Sep 02 16:41:42 2010 +0200
@@ -122,7 +122,7 @@
   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 @{theory Imperative_HOL}.
+  is available in session @{text Imperative_HOL}.
 *}