diff -r 1e31ddcab458 -r 4c275405faae src/Doc/Isar_Ref/First_Order_Logic.thy
--- a/src/Doc/Isar_Ref/First_Order_Logic.thy	Sun Jan 15 16:28:03 2023 +0100
+++ b/src/Doc/Isar_Ref/First_Order_Logic.thy	Sun Jan 15 18:30:18 2023 +0100
@@ -164,7 +164,7 @@
 text \<open>
   We axiomatize basic connectives of propositional logic: implication,
   disjunction, and conjunction. The associated rules are modeled after
-  Gentzen's system of Natural Deduction @{cite "Gentzen:1935"}.
+  Gentzen's system of Natural Deduction \<^cite>\<open>"Gentzen:1935"\<close>.
 \<close>
 
 axiomatization imp :: "o \<Rightarrow> o \<Rightarrow> o"  (infixr "\<longrightarrow>" 25)
@@ -315,7 +315,7 @@
 text \<open>
   Representing quantifiers is easy, thanks to the higher-order nature of the
   underlying framework. According to the well-known technique introduced by
-  Church @{cite "church40"}, quantifiers are operators on predicates, which
+  Church \<^cite>\<open>"church40"\<close>, quantifiers are operators on predicates, which
   are syntactically represented as \<open>\<lambda>\<close>-terms of type \<^typ>\<open>i \<Rightarrow> o\<close>. Binder
   notation turns \<open>All (\<lambda>x. B x)\<close> into \<open>\<forall>x. B x\<close> etc.
 \<close>