# HG changeset patch
# User wenzelm
# Date 1445202223 -7200
# Node ID eec2c9aee907b56139b07a0ac1e86b74c7af7443
# Parent  6e789d198bbda0af6b3ba044b64605d36dc1e22d
tuned;

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 \<open>\emph\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
+  markup @{verbatim \<open>\emph{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.
 
   \<^descr> @{text "@{bold s}"} prints document source recursively, with {\LaTeX}
   markup @{verbatim \<open>\textbf{\<close>}@{text "\<dots>"}@{verbatim \<open>}\<close>}.