diff -r 1e31ddcab458 -r 4c275405faae src/Pure/Examples/Higher_Order_Logic.thy
--- a/src/Pure/Examples/Higher_Order_Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Pure/Examples/Higher_Order_Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,7 @@
 
 text \<open>
   The following theory development illustrates the foundations of Higher-Order
-  Logic. The ``HOL'' logic that is given here resembles @{cite
-  "Gordon:1985:HOL"} and its predecessor @{cite "church40"}, but the order of
+  Logic. The ``HOL'' logic that is given here resembles \<^cite>\<open>"Gordon:1985:HOL"\<close> and its predecessor \<^cite>\<open>"church40"\<close>, but the order of
   axiomatizations and defined connectives has be adapted to modern
   presentations of \<open>\<lambda>\<close>-calculus and Constructive Type Theory. Thus it fits
   nicely to the underlying Natural Deduction framework of Isabelle/Pure and