--- 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
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Dec 30 21:05:15 2015 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Dec 30 21:10:19 2015 +0100
@@ -101,14 +101,13 @@
present), including current facts and goals.
- All of the diagnostic commands above admit a list of \<open>modes\<close>
- to be specified, which is appended to the current print mode; see
- also \secref{sec:print-modes}. Thus the output behavior may be
- modified according particular print mode features. For example,
- @{command "print_state"}~\<open>(latex xsymbols)\<close> prints the
- current proof state with mathematical symbols and special characters
- represented in {\LaTeX} source, according to the Isabelle style
- @{cite "isabelle-system"}.
+ All of the diagnostic commands above admit a list of \<open>modes\<close> to be
+ specified, which is appended to the current print mode; see also
+ \secref{sec:print-modes}. Thus the output behavior may be modified according
+ particular print mode features. For example, @{command
+ "print_state"}~\<open>(latex)\<close> prints the current proof state with mathematical
+ symbols and special characters represented in {\LaTeX} source, according to
+ the Isabelle style @{cite "isabelle-system"}.
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
systematic way to include formal items into the printed text
@@ -278,9 +277,7 @@
\<^item> \<^verbatim>\<open>internal\<close> dummy print mode that is never active;
used internally in Isabelle/Pure.
- \<^item> \<^verbatim>\<open>xsymbols\<close>: enable proper mathematical symbols
- instead of ASCII art.\<^footnote>\<open>This traditional mode name stems from
- the ``X-Symbol'' package for classic Proof~General with XEmacs.\<close>
+ \<^item> \<^verbatim>\<open>ASCII\<close>: prefer ASCII art over mathematical symbols.
\<^item> \<^verbatim>\<open>latex\<close>: additional mode that is active in {\LaTeX}
document preparation of Isabelle theory sources; allows to provide