# HG changeset patch
# User haftmann
# Date 1282048419 -7200
# Node ID 34d3de1254cdca14b837418b5debe919004479e9
# Parent  75fc4087764eaf7234b04696d7f2159cfbd3b850
formally document `code abstype` and `code abstract` attributes

diff -r 75fc4087764e -r 34d3de1254cd doc-src/IsarRef/Thy/HOL_Specific.thy
--- 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
diff -r 75fc4087764e -r 34d3de1254cd doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- 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