--- 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