diff -r 1e31ddcab458 -r 4c275405faae src/HOL/Isar_Examples/Mutilated_Checkerboard.thy
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -10,8 +10,7 @@
 begin
 
 text \<open>
-  The Mutilated Checker Board Problem, formalized inductively. See @{cite
-  "paulson-mutilated-board"} for the original tactic script version.
+  The Mutilated Checker Board Problem, formalized inductively. See \<^cite>\<open>"paulson-mutilated-board"\<close> for the original tactic script version.
 \<close>
 
 subsection \<open>Tilings\<close>