diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Imperative_HOL/Overview.thy
--- a/src/HOL/Imperative_HOL/Overview.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Imperative_HOL/Overview.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -20,8 +20,8 @@
 text \<open>
   \<open>Imperative HOL\<close> is a lightweight framework for reasoning
   about imperative data structures in \<open>Isabelle/HOL\<close>
-  @{cite "Nipkow-et-al:2002:tutorial"}.  Its basic ideas are described in
-  @{cite "Bulwahn-et-al:2008:imp_HOL"}.  However their concrete
+  \<^cite>\<open>"Nipkow-et-al:2002:tutorial"\<close>.  Its basic ideas are described in
+  \<^cite>\<open>"Bulwahn-et-al:2008:imp_HOL"\<close>.  However their concrete
   realisation has changed since, due to both extensions and
   refinements.  Therefore this overview wants to present the framework
   \qt{as it is} by now.  It focusses on the user-view, less on matters