--- a/src/Doc/Isar_Ref/Document_Preparation.thy Wed Dec 30 21:05:15 2015 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Wed Dec 30 21:10:19 2015 +0100
@@ -378,8 +378,7 @@
\<^descr> @{antiquotation_option_def mode}~\<open>= name\<close> adds \<open>name\<close> to the print mode
to be used for presentation. Note that the standard setup for {\LaTeX}
- output is already present by default, including the modes \<open>latex\<close> and
- \<open>xsymbols\<close>.
+ output is already present by default, with mode ``\<open>latex\<close>''.
\<^descr> @{antiquotation_option_def margin}~\<open>= nat\<close> and
@{antiquotation_option_def indent}~\<open>= nat\<close> change the margin or