clarified
authorhaftmann
Wed, 30 Jul 2008 07:33:56 +0200
changeset 2770610a6ede68bc8
parent 27705 f6277c8ab8ef
child 27707 54bf1fea9252
clarified
doc-src/IsarRef/Thy/HOL_Specific.thy
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 30 07:33:55 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 30 07:33:56 2008 +0200
     1.3 @@ -1063,14 +1063,14 @@
     1.4    \emph{Haskell}.
     1.5  
     1.6    \item [@{command (HOL) "code_monad"}] provides an auxiliary
     1.7 -  mechanism to generate monadic code.
     1.8 +  mechanism to generate monadic code for Haskell.
     1.9  
    1.10    \item [@{command (HOL) "code_reserved"}] declares a list of names as
    1.11    reserved for a given target, preventing it to be shadowed by any
    1.12    generated code.
    1.13  
    1.14    \item [@{command (HOL) "code_include"}] adds arbitrary named content
    1.15 -  (``include'') to generated code.  A as last argument ``@{text "-"}''
    1.16 +  (``include'') to generated code.  A ``@{text "-"}'' as last argument
    1.17    will remove an already added ``include''.
    1.18  
    1.19    \item [@{command (HOL) "code_modulename"}] declares aliasings from