doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 38462 34d3de1254cd
parent 37820 ffaca9167c16
child 38814 4d575fbfc920
     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