diff -r 9457e0133a85 -r 2ea9f9ed19c6 src/Pure/Examples/Higher_Order_Logic.thy
--- a/src/Pure/Examples/Higher_Order_Logic.thy	Sun Feb 02 00:14:26 2025 +0100
+++ b/src/Pure/Examples/Higher_Order_Logic.thy	Sun Feb 02 12:11:03 2025 +0100
@@ -9,12 +9,13 @@
 begin
 
 text \<open>
-  The following theory development illustrates the foundations of Higher-Order
-  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
-  Isabelle/Isar.
+  The following theory development illustrates the foundations of
+  Higher-Order 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 Isabelle/Isar.
 \<close>