--- a/src/Doc/IsarRef/HOL_Specific.thy Wed Jan 01 01:05:46 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy Wed Jan 01 01:05:48 2014 +0100
@@ -2391,7 +2391,6 @@
\begin{matharray}{rcl}
@{command_def (HOL) "export_code"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{attribute_def (HOL) code} & : & @{text attribute} \\
- @{command_def (HOL) "code_abort"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "code_datatype"} & : & @{text "theory \<rightarrow> theory"} \\
@{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{attribute_def (HOL) code_unfold} & : & @{text attribute} \\
@@ -2435,10 +2434,8 @@
target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
;
- @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract' )?
- ;
-
- @@{command (HOL) code_abort} ( const + )
+ @@{attribute (HOL) code} ( 'del' | 'equation' | 'abstype' | 'abstract'
+ | 'drop:' ( const + ) | 'abort:' ( const + ) )?
;
@@{command (HOL) code_datatype} ( const + )
@@ -2600,13 +2597,15 @@
of the underlying equation. Variant @{text "code del"}
deselects a code equation for code generation.
+ Variants @{text "code drop:"} and @{text "code abort:"} take
+ a list of constant as arguments and drop all code equations declared
+ for them. In the case of {text abort}, these constants then are
+ are not required to have a definition by means of code equations;
+ if needed these are implemented by program abort (exception) instead.
+
Usually packages introducing code equations provide a reasonable
default setup for selection.
- \item @{command (HOL) "code_abort"} declares constants which are not
- required to have a definition by means of code equations; if needed
- these are implemented by program abort instead.
-
\item @{command (HOL) "code_datatype"} specifies a constructor set
for a logical type.