# HG changeset patch
# User wenzelm
# Date 1645984730 -3600
# Node ID d48998648281edde3d9e7bf7dbb5997840cf7990
# Parent  1994ee39e513fe91424dd62f413e88bf753fd38b
misc tuning based on comments by Heiko Eißfeldt;

diff -r 1994ee39e513 -r d48998648281 src/Doc/Eisbach/Manual.thy
--- 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](*>*)
diff -r 1994ee39e513 -r d48998648281 src/Doc/Eisbach/Preface.thy
--- 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>