--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 24 17:48:39 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Oct 24 17:48:40 2008 +0200
@@ -1050,9 +1050,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 [@{command (HOL) "code_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 [@{command (HOL) "code_instance"}] declares a list of type
constructor / class instance relations as ``already present'' for a