doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 31998 2c7a24f74db9
parent 31912 f5bd306f5e9d
child 33857 0cb5002c52db
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 10:53:44 2009 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jul 14 10:54:04 2009 +0200
     1.3 @@ -1190,7 +1190,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 @@ -1280,11 +1286,15 @@
    1.19    generation.  Usually packages introducing code equations provide
    1.20    a reasonable default setup for selection.
    1.21  
    1.22 -  \item @{attribute (HOL) code}~@{text inline} declares (or with
    1.23 +  \item @{attribute (HOL) code_inline} declares (or with
    1.24    option ``@{text "del"}'' removes) inlining theorems which are
    1.25    applied as rewrite rules to any code equation during
    1.26    preprocessing.
    1.27  
    1.28 +  \item @{attribute (HOL) code_post} declares (or with
    1.29 +  option ``@{text "del"}'' removes) theorems which are
    1.30 +  applied as rewrite rules to any result of an evaluation.
    1.31 +
    1.32    \item @{command (HOL) "print_codesetup"} gives an overview on
    1.33    selected code equations and code generator datatypes.
    1.34