--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jun 10 15:30:01 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Tue Jun 10 15:30:06 2008 +0200
@@ -915,7 +915,7 @@
@{command_def (HOL) "code_reserved"} & : & \isartrans{theory}{theory} \\
@{command_def (HOL) "code_include"} & : & \isartrans{theory}{theory} \\
@{command_def (HOL) "code_modulename"} & : & \isartrans{theory}{theory} \\
- @{command_def (HOL) "code_exception"} & : & \isartrans{theory}{theory} \\
+ @{command_def (HOL) "code_abort"} & : & \isartrans{theory}{theory} \\
@{command_def (HOL) "print_codesetup"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
@{attribute_def (HOL) code} & : & \isaratt \\
\end{matharray}
@@ -1069,9 +1069,9 @@
\item [@{command (HOL) "code_modulename"}] declares aliasings from
one module name onto another.
- \item [@{command (HOL) "code_exception"}] declares constants which
- are not required to have a definition by a defining equations; these
- are mapped on exceptions instead.
+ \item [@{command (HOL) "code_abort"}] declares constants which
+ are not required to have a definition by a defining equations;
+ if needed these are implemented by program abort instead.
\item [@{attribute (HOL) code}~@{text func}] explicitly selects (or
with option ``@{text "del:"}'' deselects) a defining equation for