--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 14:33:39 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Aug 17 14:33:39 2010 +0200
@@ -1018,7 +1018,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1104,9 +1104,11 @@
declaration.
\item @{attribute (HOL) code} explicitly selects (or with option
- ``@{text "del"}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``@{text "del"}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants @{text "code abstype"} and
+ @{text "code abstract"} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item @{command (HOL) "code_abort"} declares constants which are not
required to have a definition by means of code equations; if
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 14:33:39 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Tue Aug 17 14:33:39 2010 +0200
@@ -1034,7 +1034,7 @@
target: 'OCaml' | 'SML' | 'Haskell'
;
- 'code' ( 'del' ) ?
+ 'code' ( 'del' | 'abstype' | 'abstract' ) ?
;
'code\_abort' ( const + )
@@ -1117,9 +1117,11 @@
declaration.
\item \hyperlink{attribute.HOL.code}{\mbox{\isa{code}}} explicitly selects (or with option
- ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code
- generation. Usually packages introducing code equations provide
- a reasonable default setup for selection.
+ ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a code equation for code generation.
+ Usually packages introducing code equations provide a reasonable
+ default setup for selection. Variants \isa{{\isachardoublequote}code\ abstype{\isachardoublequote}} and
+ \isa{{\isachardoublequote}code\ abstract{\isachardoublequote}} declare abstract datatype certificates or
+ code equations on abstract datatype representations respectively.
\item \hyperlink{command.HOL.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}} declares constants which are not
required to have a definition by means of code equations; if