doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 28687 150a8a1eae1a
parent 28603 b40800eef8a7
child 28788 ff9d8a8932e4
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 24 17:48:39 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Oct 24 17:48:40 2008 +0200
     1.3 @@ -1053,9 +1053,7 @@
     1.4      ;
     1.5  
     1.6      'code\_class' (class + 'and') \\
     1.7 -      ( ( '(' target \\
     1.8 -        ( ( string ('where' \\
     1.9 -          ( const ( '==' | equiv ) string ) + ) ? ) ? + 'and' ) ')' ) + )
    1.10 +      ( ( '(' target \\ ( string ? + 'and' ) ')' ) + )
    1.11      ;
    1.12  
    1.13      'code\_instance' (( typeconstructor '::' class ) + 'and') \\
    1.14 @@ -1135,10 +1133,9 @@
    1.15    serialization deletes an existing serialization.
    1.16  
    1.17    \item [\hyperlink{command.HOL.code-class}{\mbox{\isa{\isacommand{code{\isacharunderscore}class}}}}] associates a list of classes
    1.18 -  with target-specific class names; in addition, constants associated
    1.19 -  with this class may be given target-specific names used for instance
    1.20 -  declarations; omitting a serialization deletes an existing
    1.21 -  serialization.  This applies only to \emph{Haskell}.
    1.22 +  with target-specific class names; omitting a
    1.23 +  serialization deletes an existing serialization.
    1.24 +  This applies only to \emph{Haskell}.
    1.25  
    1.26    \item [\hyperlink{command.HOL.code-instance}{\mbox{\isa{\isacommand{code{\isacharunderscore}instance}}}}] declares a list of type
    1.27    constructor / class instance relations as ``already present'' for a