tuned;
authorwenzelm
Fri, 04 Oct 2024 13:22:35 +0200
changeset 81112 d9e3161080f9
parent 81111 f1a3a553e8cf
child 81113 6fefd6c602fa
tuned;
src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Oct 04 00:26:28 2024 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Fri Oct 04 13:22:35 2024 +0200
@@ -358,7 +358,7 @@
   The argument syntax is uniform for all variants and is usually presented in
   control-symbol-cartouche form: \<open>\<^cite>\<open>arg\<close>\<close>. The formal syntax of the
   nested argument language is defined as follows: \<^rail>\<open>arg: (embedded
-  @'in')? (name + 'and') \<newline> (@'using' name)?\<close>
+  @'in')? (name + @'and') \<newline> (@'using' name)?\<close>
 
   Here the embedded text is free-form {\LaTeX}, which becomes the optional
   argument of the \<^verbatim>\<open>\cite\<close> macro. The named items are Bib{\TeX} database