1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 14:33:39 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Aug 17 14:33:39 2010 +0200
     1.3 @@ -1018,7 +1018,7 @@
     1.4      target: 'OCaml' | 'SML' | 'Haskell'
     1.5      ;
     1.6  
     1.7 -    'code' ( 'del' ) ?
     1.8 +    'code' ( 'del' | 'abstype' | 'abstract' ) ?
     1.9      ;
    1.10  
    1.11      'code\_abort' ( const + )
    1.12 @@ -1104,9 +1104,11 @@
    1.13    declaration.
    1.14  
    1.15    \item @{attribute (HOL) code} explicitly selects (or with option
    1.16 -  ``@{text "del"}'' deselects) a code equation for code
    1.17 -  generation.  Usually packages introducing code equations provide
    1.18 -  a reasonable default setup for selection.
    1.19 +  ``@{text "del"}'' deselects) a code equation for code generation.
    1.20 +  Usually packages introducing code equations provide a reasonable
    1.21 +  default setup for selection.  Variants @{text "code abstype"} and
    1.22 +  @{text "code abstract"} declare abstract datatype certificates or
    1.23 +  code equations on abstract datatype representations respectively.
    1.24  
    1.25    \item @{command (HOL) "code_abort"} declares constants which are not
    1.26    required to have a definition by means of code equations; if

     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 14:33:39 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 14:33:39 2010 +0200
     2.3 @@ -1034,7 +1034,7 @@
     2.4      target: 'OCaml' | 'SML' | 'Haskell'
     2.5      ;
     2.6  
     2.7 -    'code' ( 'del' ) ?
     2.8 +    'code' ( 'del' | 'abstype' | 'abstract' ) ?
     2.9      ;
    2.10  
    2.11      'code\_abort' ( const + )
    2.12 @@ -1117,9 +1117,11 @@
    2.13    declaration.
    2.14  
    2.15    \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
    2.16 -  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
    2.17 -  generation.  Usually packages introducing code equations provide
    2.18 -  a reasonable default setup for selection.
    2.19 +  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
    2.20 +  Usually packages introducing code equations provide a reasonable
    2.21 +  default setup for selection.  Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
    2.22 +  \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
    2.23 +  code equations on abstract datatype representations respectively.
    2.24  
    2.25    \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
    2.26    required to have a definition by means of code equations; if