--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Aug 11 22:25:45 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 12 21:27:46 2008 +0200
@@ -1064,14 +1064,14 @@
\emph{Haskell}.
\item [\hyperlink{command.HOL.code-monad}{\mbox{\isa{\isacommand{code{\isacharunderscore}monad}}}}] provides an auxiliary
- mechanism to generate monadic code.
+ mechanism to generate monadic code for Haskell.
\item [\hyperlink{command.HOL.code-reserved}{\mbox{\isa{\isacommand{code{\isacharunderscore}reserved}}}}] declares a list of names as
reserved for a given target, preventing it to be shadowed by any
generated code.
\item [\hyperlink{command.HOL.code-include}{\mbox{\isa{\isacommand{code{\isacharunderscore}include}}}}] adds arbitrary named content
- (``include'') to generated code. A as last argument ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}''
+ (``include'') to generated code. A ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' as last argument
will remove an already added ``include''.
\item [\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}] declares aliasings from