diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/Outer_Syntax.thy --- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Jan 15 16:28:03 2023 +0100 +++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sun Jan 15 18:30:18 2023 +0100 @@ -26,8 +26,7 @@ theory, while \<^verbatim>\x + y\ without quotes is not. Printed theory documents usually omit quotes to gain readability (this is a - matter of {\LaTeX} macro setup, say via \<^verbatim>\\isabellestyle\, see also @{cite - "isabelle-system"}). Experienced users of Isabelle/Isar may easily + matter of {\LaTeX} macro setup, say via \<^verbatim>\\isabellestyle\, see also \<^cite>\"isabelle-system"\). Experienced users of Isabelle/Isar may easily reconstruct the lost technical information, while mere readers need not care about quotes at all. \