doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 28562 4e74209f113e
parent 27706 10a6ede68bc8
child 28603 b40800eef8a7
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -993,7 +993,7 @@
     1.4      syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     1.5      ;
     1.6  
     1.7 -    'code' ('func' | 'inline') ( 'del' )?
     1.8 +    'code' ( 'inline' ) ? ( 'del' ) ?
     1.9      ;
    1.10    \end{rail}
    1.11  
    1.12 @@ -1080,13 +1080,13 @@
    1.13    are not required to have a definition by means of defining equations;
    1.14    if needed these are implemented by program abort instead.
    1.15  
    1.16 -  \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
    1.17 -  with option ``@{text "del:"}'' deselects) a defining equation for
    1.18 +  \item [@{attribute (HOL) code}] explicitly selects (or
    1.19 +  with option ``@{text "del"}'' deselects) a defining equation for
    1.20    code generation.  Usually packages introducing defining equations
    1.21    provide a reasonable default setup for selection.
    1.22  
    1.23    \item [@{attribute (HOL) code}@{text inline}] declares (or with
    1.24 -  option ``@{text "del:"}'' removes) inlining theorems which are
    1.25 +  option ``@{text "del"}'' removes) inlining theorems which are
    1.26    applied as rewrite rules to any defining equation during
    1.27    preprocessing.
    1.28