diff -r f1a3a553e8cf -r d9e3161080f9 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: \\<^cite>\arg\\. The formal syntax of the nested argument language is defined as follows: \<^rail>\arg: (embedded - @'in')? (name + 'and') \ (@'using' name)?\ + @'in')? (name + @'and') \ (@'using' name)?\ Here the embedded text is free-form {\LaTeX}, which becomes the optional argument of the \<^verbatim>\\cite\ macro. The named items are Bib{\TeX} database