# HG changeset patch
# User wenzelm
# Date 1451506219 -3600
# Node ID 4d9518c3d031cff68adb1aa7fbd6c99acd7ec874
# Parent  208c99a0092ece58cfd3e884ac9e2d56b1a3e9d5
updated print modes;

diff -r 208c99a0092e -r 4d9518c3d031 src/Doc/Isar_Ref/Document_Preparation.thy
--- 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
diff -r 208c99a0092e -r 4d9518c3d031 src/Doc/Isar_Ref/Inner_Syntax.thy
--- 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