doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 31248 03a35fbc9dc6
parent 30865 5106e13d400f
child 31906 f5bd306f5e9d
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon May 25 22:14:59 2009 -0700
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue May 26 12:31:01 2009 +0200
     1.3 @@ -1065,6 +1065,7 @@
     1.4      @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
     1.5      @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
     1.6      @{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.7 +    @{command_def (HOL) "print_codeproc"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     1.8      @{attribute_def (HOL) code} & : & @{text attribute} \\
     1.9    \end{matharray}
    1.10  
    1.11 @@ -1228,8 +1229,10 @@
    1.12    preprocessing.
    1.13  
    1.14    \item @{command (HOL) "print_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 @{command (HOL) "print_codeproc"} prints the setup
    1.20 +  of the code generator preprocessor.
    1.21  
    1.22    \end{description}
    1.23  *}