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