doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 31254 03a35fbc9dc6
parent 30865 5106e13d400f
child 31913 edce86bf8521
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon May 25 22:14:59 2009 -0700
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue May 26 12:31:01 2009 +0200
     1.3 @@ -1074,6 +1074,7 @@
     1.4      \indexdef{HOL}{command}{code\_modulename}\hypertarget{command.HOL.code-modulename}{\hyperlink{command.HOL.code-modulename}{\mbox{\isa{\isacommand{code{\isacharunderscore}modulename}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.5      \indexdef{HOL}{command}{code\_abort}\hypertarget{command.HOL.code-abort}{\hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.6      \indexdef{HOL}{command}{print\_codesetup}\hypertarget{command.HOL.print-codesetup}{\hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.7 +    \indexdef{HOL}{command}{print\_codeproc}\hypertarget{command.HOL.print-codeproc}{\hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.8      \indexdef{HOL}{attribute}{code}\hypertarget{attribute.HOL.code}{\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}} & : & \isa{attribute} \\
     1.9    \end{matharray}
    1.10  
    1.11 @@ -1234,8 +1235,10 @@
    1.12    preprocessing.
    1.13  
    1.14    \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
    1.15 -  selected code equations, code generator datatypes and
    1.16 -  preprocessor setup.
    1.17 +  selected code equations and code generator datatypes.
    1.18 +
    1.19 +  \item \hyperlink{command.HOL.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} prints the setup
    1.20 +  of the code generator preprocessor.
    1.21  
    1.22    \end{description}%
    1.23  \end{isamarkuptext}%