doc-src/IsarRef/Thy/HOL_Specific.thy

     ;
 
     syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
     ;
 
-    'code' ('func' | 'inline') ( 'del' )?
+    'code' ( 'inline' ) ? ( 'del' ) ?
     ;
   \end{rail}
 
   \begin{descr}
 

 
   \item [@{command (HOL) "code_abort"}] declares constants which
   are not required to have a definition by means of defining equations;
   if needed these are implemented by program abort instead.
 
-  \item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
-  with option ``@{text "del:"}'' deselects) a defining equation for
+  \item [@{attribute (HOL) code}] explicitly selects (or
+  with option ``@{text "del"}'' deselects) a defining equation for
   code generation.  Usually packages introducing defining equations
   provide a reasonable default setup for selection.
 
   \item [@{attribute (HOL) code}@{text inline}] declares (or with
-  option ``@{text "del:"}'' removes) inlining theorems which are
+  option ``@{text "del"}'' removes) inlining theorems which are
   applied as rewrite rules to any defining equation during
   preprocessing.
 
   \item [@{command (HOL) "print_codesetup"}] gives an overview on
   selected defining equations, code generator datatypes and