--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 10 06:45:50 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 10 06:45:53 2008 +0200
@@ -997,7 +997,7 @@
syntax: string | ( 'infix' | 'infixl' | 'infixr' ) nat string
;
- 'code' ('func' | 'inline') ( 'del' )?
+ 'code' ( 'inline' ) ? ( 'del' ) ?
;
\end{rail}
@@ -1081,13 +1081,13 @@
are not required to have a definition by means of defining equations;
if needed these are implemented by program abort instead.
- \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}~\isa{func}] explicitly selects (or
- with option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' deselects) a defining equation for
+ \item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}] explicitly selects (or
+ with option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' deselects) a defining equation for
code generation. Usually packages introducing defining equations
provide a reasonable default setup for selection.
\item [\hyperlink{attribute.HOL.code}{\mbox{\isa{code}}}\isa{inline}] declares (or with
- option ``\isa{{\isachardoublequote}del{\isacharcolon}{\isachardoublequote}}'' removes) inlining theorems which are
+ option ``\isa{{\isachardoublequote}del{\isachardoublequote}}'' removes) inlining theorems which are
applied as rewrite rules to any defining equation during
preprocessing.