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