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