# HG changeset patch
# User wenzelm
# Date 1738494663 -3600
# Node ID 2ea9f9ed19c65fafbec86d5fab2ea90ae1b94e7f
# Parent  9457e0133a851606dec434a8c19402c25e585bae
tuned;

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>
 
 
diff -r 9457e0133a85 -r 2ea9f9ed19c6 src/Pure/ex/Guess.thy
--- a/src/Pure/ex/Guess.thy	Sun Feb 02 00:14:26 2025 +0100
+++ b/src/Pure/ex/Guess.thy	Sun Feb 02 12:11:03 2025 +0100
@@ -26,10 +26,10 @@
 begin
 
 text \<open>
-  The @{command guess} is similar to @{command obtain}, but it derives the
-  obtained context elements from the course of tactical reasoning in the
-  proof. Thus it can considerably obscure the proof: it is provided here as
-  \<^emph>\<open>improper\<close> and experimental feature.
+  The is similar to @{command obtain}, but it derives the obtained context
+  elements from the course of tactical reasoning in the proof. Thus it can
+  considerably obscure the proof: it is provided here as \<^emph>\<open>improper\<close> and
+  experimental feature.
 
   A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The
   subsequent refinement steps may turn this to anything of the form