diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Isar_Examples/Basic_Logic.thy
--- a/src/HOL/Isar_Examples/Basic_Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Basic_Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -250,8 +250,7 @@
 subsection \<open>A few examples from ``Introduction to Isabelle''\<close>
 
 text \<open>
-  We rephrase some of the basic reasoning examples of @{cite
-  "isabelle-intro"}, using HOL rather than FOL.
+  We rephrase some of the basic reasoning examples of \<^cite>\<open>"isabelle-intro"\<close>, using HOL rather than FOL.
 \<close>