diff -r 6e789d198bbd -r eec2c9aee907 src/Doc/Isar_Ref/Document_Preparation.thy --- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 23:00:32 2015 +0200 +++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun Oct 18 23:03:43 2015 +0200 @@ -270,7 +270,7 @@ and functor respectively. The source is printed verbatim. \<^descr> @{text "@{emph s}"} prints document source recursively, with {\LaTeX} - markup @{verbatim \\emph\}@{text "\"}@{verbatim \}\}. + markup @{verbatim \\emph{\}@{text "\"}@{verbatim \}\}. \<^descr> @{text "@{bold s}"} prints document source recursively, with {\LaTeX} markup @{verbatim \\textbf{\}@{text "\"}@{verbatim \}\}.