diff -r 760e21900b01 -r 28e788ca2c5d src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Oct 22 21:16:27 2015 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Oct 22 21:16:49 2015 +0200 @@ -2469,9 +2469,9 @@ hierarchy. Omitting the file specification denotes standard output. Serializers take an optional list of arguments in parentheses. For - \<^emph>\Haskell\ a module name prefix may be given using the ``\root:\'' argument; ``\string_classes\'' adds a ``@{verbatim - "deriving (Read, Show)"}'' clause to each appropriate datatype - declaration. + \<^emph>\Haskell\ a module name prefix may be given using the ``\root:\'' argument; + ``\string_classes\'' adds a ``\<^verbatim>\deriving (Read, Show)\'' clause to each + appropriate datatype declaration. \<^descr> @{attribute (HOL) code} declare code equations for code generation. Variant \code equation\ declares a conventional equation as code