1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -1201,7 +1201,13 @@
     1.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     1.5      ;
     1.6  
     1.7 -    'code' ( 'inline' ) ? ( 'del' ) ?
     1.8 +    'code' ( 'del' ) ?
     1.9 +    ;
    1.10 +
    1.11 +    'code_unfold' ( 'del' ) ?
    1.12 +    ;
    1.13 +
    1.14 +    'code_post' ( 'del' ) ?
    1.15      ;
    1.16    \end{rail}
    1.17  
    1.18 @@ -1288,11 +1294,15 @@
    1.19    generation.  Usually packages introducing code equations provide
    1.20    a reasonable default setup for selection.
    1.21  
    1.22 -  \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{inline} declares (or with
    1.23 +  \item \hyperlink{attribute.HOL.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} declares (or with
    1.24    option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
    1.25    applied as rewrite rules to any code equation during
    1.26    preprocessing.
    1.27  
    1.28 +  \item \hyperlink{attribute.HOL.code-post}{\mbox{\isa{code{\isacharunderscore}post}}} declares (or with
    1.29 +  option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) theorems which are
    1.30 +  applied as rewrite rules to any result of an evaluation.
    1.31 +
    1.32    \item \hyperlink{command.HOL.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} gives an overview on
    1.33    selected code equations and code generator datatypes.
    1.34