--- a/src/Doc/Eisbach/Manual.thy Sat Feb 26 22:00:22 2022 +0100
+++ b/src/Doc/Eisbach/Manual.thy Sun Feb 27 18:58:50 2022 +0100
@@ -101,9 +101,9 @@
text \<open>
A \<^emph>\<open>named theorem\<close> is a fact whose contents are produced dynamically within
the current proof context. The Isar command @{command_ref "named_theorems"}
- provides simple access to this concept: it declares a dynamic fact with
- corresponding \<^emph>\<open>attribute\<close> for managing this particular data slot in the
- context.
+ declares a dynamic fact with a corresponding \<^emph>\<open>attribute\<close> of the same
+ name. This allows to maintain a collection of facts in the context as
+ follows:
\<close>
named_theorems intros
@@ -171,8 +171,8 @@
text \<open>
The \<^emph>\<open>structured concatenation\<close> combinator ``\<open>method\<^sub>1 ; method\<^sub>2\<close>'' was
- introduced in Isabelle2015, motivated by development of Eisbach. It is
- similar to ``\<open>method\<^sub>1, method\<^sub>2\<close>'', but \<open>method\<^sub>2\<close> is invoked on on \<^emph>\<open>all\<close>
+ introduced in Isabelle2015, motivated by the development of Eisbach. It is
+ similar to ``\<open>method\<^sub>1, method\<^sub>2\<close>'', but \<open>method\<^sub>2\<close> is invoked on \<^emph>\<open>all\<close>
subgoals that have newly emerged from \<open>method\<^sub>1\<close>. This is useful to handle
cases where the number of subgoals produced by a method is determined
dynamically at run-time.
@@ -493,7 +493,7 @@
text \<open>
Attributes may throw errors when applied to a given fact. For example, rule
- instantiation will fail of there is a type mismatch or if a given variable
+ instantiation will fail if there is a type mismatch or if a given variable
doesn't exist. Within a match or a method definition, it isn't generally
possible to guarantee that applied attributes won't fail. For example, in
the following method there is no guarantee that the two provided facts will
@@ -933,7 +933,7 @@
function of the same name into an attribute. When applied to a case
distinction over a datatype, it retrieves its corresponding split rule.
- We can then integrate this intro a method that applies the split rule, first
+ We can then integrate this into a method that applies the split rule, first
matching to ensure that fetching the rule was successful.
\<close>
(*<*)declare TrueI [intros](*>*)
--- a/src/Doc/Eisbach/Preface.thy Sat Feb 26 22:00:22 2022 +0100
+++ b/src/Doc/Eisbach/Preface.thy Sun Feb 27 18:58:50 2022 +0100
@@ -22,18 +22,20 @@
written. For example, the @{method catch} method, which provides basic
try-catch functionality, only requires a few lines of ML.
- Eisbach is meant to allow users to write automation using only Isar syntax.
- Traditionally proof methods have been written in Isabelle/ML, which poses a
- high barrier-to-entry for many users.
+ Eisbach enables users to implement automated proof tools conveniently via
+ Isabelle/Isar syntax. This is in contrast to the traditional approach to use
+ Isabelle/ML (via @{command_ref method_setup}), which poses a higher
+ barrier-to-entry for casual users.
\<^medskip>
- This manual is written for users familiar with Isabelle/Isar, but not
+ This manual is written for readers familiar with Isabelle/Isar, but not
necessarily Isabelle/ML. It covers the usage of the @{command method} as
well as the @{method match} method, as well as discussing their integration
with existing Isar concepts such as @{command named_theorems}.
These commands are provided by theory \<^theory>\<open>HOL-Eisbach.Eisbach\<close>: it
- needs to be imported by all Eisbach applications. Theory theory \<^theory>\<open>HOL-Eisbach.Eisbach_Tools\<close> provides additional proof methods and
+ needs to be imported by all Eisbach applications. Theory
+ \<^theory>\<open>HOL-Eisbach.Eisbach_Tools\<close> provides additional proof methods and
attributes that are occasionally useful.
\<close>