# HG changeset patch
# User wenzelm
# Date 1730028228 -3600
# Node ID 5e4a3237fc868c849af14f82954a26623b6cddc3
# Parent  d96c9cd44b608650762d5d75167f75e3d48a5e3b
update documentation: print mode "latex" only affects syntax tables, but output of symbols;

diff -r d96c9cd44b60 -r 5e4a3237fc86 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Oct 27 12:13:34 2024 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sun Oct 27 12:23:48 2024 +0100
@@ -94,16 +94,12 @@
     \<^descr> @{command "print_state"} prints the current proof state (if 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)\<close> prints the current proof state with mathematical
-  symbols and special characters represented in {\LaTeX} source, according to
-  the Isabelle style \<^cite>\<open>"isabelle-system"\<close>.
-
-  Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more systematic
-  way to include formal items into the printed text document.
+  The diagnostic commands above accept an optional list of \<open>modes\<close>, 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 "thm"}~\<^verbatim>\<open>("") symmetric\<close> prints a theorem
+  without any special markup, bypassing the print mode setup of the Prover
+  IDE.
 \<close>