# HG changeset patch
# User wenzelm
# Date 1584548960 -3600
# Node ID 9a29e883a93471da7d434d637e6c402fb27f2d12
# Parent  76b739c0bedd7c7a3a24aef9dd5bde57fb34bd86
tuned documentation, based on hints by Pedro Sánchez Terraf;

diff -r 76b739c0bedd -r 9a29e883a934 src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Wed Mar 18 16:46:07 2020 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy	Wed Mar 18 17:29:20 2020 +0100
@@ -1301,8 +1301,8 @@
 
   The rule \<open>P \<Longrightarrow> P \<or> Q\<close> is unsafe because it reduces \<open>P
   \<or> Q\<close> to \<open>P\<close>, which might turn out as premature choice of an
-  unprovable subgoal.  Any rule is unsafe whose premises contain new
-  unknowns.  The elimination rule \<open>\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q\<close> is
+  unprovable subgoal.  Any rule whose premises contain new unknowns is
+  unsafe. The elimination rule \<open>\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q\<close> is
   unsafe, since it is applied via elim-resolution, which discards the
   assumption \<open>\<forall>x. P x\<close> and replaces it by the weaker
   assumption \<open>P t\<close>.  The rule \<open>P t \<Longrightarrow> \<exists>x. P x\<close> is
@@ -1316,8 +1316,8 @@
   that \<open>(\<or>E)\<close> is unsafe, because repeated application of it
   could generate exponentially many subgoals.  Induction rules are
   unsafe because inductive proofs are difficult to set up
-  automatically.  Any inference is unsafe that instantiates an unknown
-  in the proof state --- thus matching must be used, rather than
+  automatically.  Any inference that instantiates an unknown
+  in the proof state is unsafe --- thus matching must be used, rather than
   unification.  Even proof by assumption is unsafe if it instantiates
   unknowns shared with other subgoals.
 
diff -r 76b739c0bedd -r 9a29e883a934 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Mar 18 16:46:07 2020 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Mar 18 17:29:20 2020 +0100
@@ -2434,7 +2434,7 @@
   Variant \<open>code nbe\<close> accepts also non-left-linear equations for
   \<^emph>\<open>normalization by evaluation\<close> only.
 
-  Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constant as arguments
+  Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constants as arguments
   and drop all code equations declared for them. In the case of \<open>abort\<close>,
   these constants then do not require to a specification by means of
   code equations; if needed these are implemented by program abort (exception)
diff -r 76b739c0bedd -r 9a29e883a934 src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Wed Mar 18 16:46:07 2020 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy	Wed Mar 18 17:29:20 2020 +0100
@@ -1190,10 +1190,10 @@
   declared using the @{attribute_def induct_simp} attribute.
 
   The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' specification generalizes variables
-  \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. One can
-  separate variables by ``\<open>and\<close>'' to generalize them in other goals then the
-  first. Thus induction hypotheses may become sufficiently general to get the
-  proof through. Together with definitional instantiations, one may
+  \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of the original goal before applying induction. It is possible
+  to separate variables by ``\<open>and\<close>'' to generalize in goals other than
+  the first. Thus induction hypotheses may become sufficiently general to get
+  the proof through. Together with definitional instantiations, one may
   effectively perform induction over expressions of a certain structure.
 
   The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' specification provides additional
diff -r 76b739c0bedd -r 9a29e883a934 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Mar 18 16:46:07 2020 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Mar 18 17:29:20 2020 +0100
@@ -194,7 +194,7 @@
   arguments; a syntactic abbreviation links the long form with the abstract
   version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>
   t[?x]\<close> at the theory level (for arbitrary \<open>?x\<close>), together with a local
-  abbreviation \<open>c \<equiv> c.a x\<close> in the target context (for the fixed parameter
+  abbreviation \<open>a \<equiv> c.a x\<close> in the target context (for the fixed parameter
   \<open>x\<close>).
 
   Theorems are exported by discharging the assumptions and generalizing the
@@ -365,7 +365,7 @@
   \<^descr> \<^theory_text>\<open>axiomatization c\<^sub>1 \<dots> c\<^sub>m where \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> introduces several constants
   simultaneously and states axiomatic properties for these. The constants are
   marked as being specified once and for all, which prevents additional
-  specifications for the same constants later on, but it is always possible do
+  specifications for the same constants later on, but it is always possible to
   emit axiomatizations without referring to particular constants. Note that
   lack of precise dependency tracking of axiomatizations may disrupt the
   well-formedness of an otherwise definitional theory.
@@ -542,7 +542,7 @@
   expressions automatically takes care of the most general typing that the
   combined context elements may acquire.
 
-  The \<open>import\<close> consists of a locale expression; see \secref{sec:proof-context}
+  The \<open>import\<close> consists of a locale expression; see \secref{sec:locale-expr}
   above. Its \<^theory_text>\<open>for\<close> clause defines the parameters of \<open>import\<close>. These are
   parameters of the defined locale. Locale parameters whose instantiation is
   omitted automatically extend the (possibly empty) \<^theory_text>\<open>for\<close> clause: they are
@@ -949,7 +949,7 @@
 
   \<^medskip>
   Co-regularity is a very fundamental property of the order-sorted algebra of
-  types. For example, it entails principle types and most general unifiers,
+  types. For example, it entails principal types and most general unifiers,
   e.g.\ see @{cite "nipkow-prehofer"}.
 \<close>