# HG changeset patch
# User wenzelm
# Date 1673873283 -3600
# Node ID a6d147b22b9b3c46934d00acc470ef0910a354f0
# Parent  11c0747a87fc477e4df0820f25d186c767d351bc
clarified documentation: avoid odd speculations about PIDE;

diff -r 11c0747a87fc -r a6d147b22b9b src/Doc/Isar_Ref/Document_Preparation.thy
--- 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.