--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun Jan 15 20:38:27 2023 +0100
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Mon Jan 16 13:48:03 2023 +0100
@@ -359,11 +359,6 @@
entries and become the mandatory argument (separated by comma). The optional
part ``\<^theory_text>\<open>using name\<close>'' specifies an alternative {\LaTeX} macro name.
- The validity of Bib{\TeX} database entries is only partially checked in
- Isabelle/PIDE, when the corresponding \<^verbatim>\<open>.bib\<close> files are open. Ultimately,
- the \<^verbatim>\<open>bibtex\<close> program will complain about bad input in final document
- preparation.
-
\<^descr> @{command "print_antiquotations"} prints all document antiquotations that
are defined in the current context; the ``\<open>!\<close>'' option indicates extra
verbosity.