1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 14:33:39 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Aug 17 14:33:39 2010 +0200
     1.3 @@ -1034,7 +1034,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 @@ -1117,9 +1117,11 @@
    1.13    declaration.
    1.14  
    1.15    \item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
    1.16 -  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' 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 +  ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
    1.20 +  Usually packages introducing code equations provide a reasonable
    1.21 +  default setup for selection.  Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
    1.22 +  \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
    1.23 +  code equations on abstract datatype representations respectively.
    1.24  
    1.25    \item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
    1.26    required to have a definition by means of code equations; if