--- a/src/Doc/Prog_Prove/Logic.thy Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Sun Jan 15 18:30:18 2023 +0100
@@ -141,7 +141,7 @@
@{thm image_def}\index{$IMP042@\<^term>\<open>f ` A\<close>} & is the image of a function over a set
\end{tabular}
\end{center}
-See @{cite "Nipkow-Main"} for the wealth of further predefined functions in theory
+See \<^cite>\<open>"Nipkow-Main"\<close> for the wealth of further predefined functions in theory
\<^theory>\<open>Main\<close>.
@@ -399,7 +399,7 @@
{\mbox{\<open>?P = ?Q\<close>}}
\]
These rules are part of the logical system of \concept{natural deduction}
-(e.g., @{cite HuthRyan}). Although we intentionally de-emphasize the basic rules
+(e.g., \<^cite>\<open>HuthRyan\<close>). Although we intentionally de-emphasize the basic rules
of logic in favour of automatic proof methods that allow you to take bigger
steps, these rules are helpful in locating where and why automation fails.
When applied backwards, these rules decompose the goal:
@@ -483,7 +483,7 @@
%
%Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
%theory. Search criteria include pattern matching on terms and on names.
-%For details see the Isabelle/Isar Reference Manual~@{cite IsarRef}.
+%For details see the Isabelle/Isar Reference Manual~\<^cite>\<open>IsarRef\<close>.
%\bigskip
\begin{warn}