--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 24 17:48:39 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Oct 24 17:48:40 2008 +0200
@@ -1053,9 +1053,7 @@
;
'code\_class' (class + 'and') \\
- ( ( '(' target \\
- ( ( string ('where' \\
- ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
+ ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
;
'code\_instance' (( typeconstructor '::' class ) + 'and') \\
@@ -1135,10 +1133,9 @@
serialization deletes an existing serialization.
\item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
- with target-specific class names; in addition, constants associated
- with this class may be given target-specific names used for instance
- declarations; omitting a serialization deletes an existing
- serialization. This applies only to \emph{Haskell}.
+ with target-specific class names; omitting a
+ serialization deletes an existing serialization.
+ This applies only to \emph{Haskell}.
\item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
constructor / class instance relations as ``already present'' for a