--- a/src/Doc/Isar_Ref/Proof.thy Thu Apr 29 22:39:33 2021 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Sat May 01 11:54:09 2021 +0200
@@ -1095,11 +1095,10 @@
This accommodates compact proof texts even when reasoning about large
specifications.
- The @{method induct} method also provides some additional infrastructure in
- order to be applicable to structure statements (either using explicit
- meta-level connectives, or including facts and parameters separately). This
- avoids cumbersome encoding of ``strengthened'' inductive statements within
- the object-logic.
+ The @{method induct} method also provides some infrastructure to work with
+ structured statements (either using explicit meta-level connectives, or
+ including facts and parameters separately). This avoids cumbersome encoding
+ of ``strengthened'' inductive statements within the object-logic.
Method @{method induction} differs from @{method induct} only in the names
of the facts in the local context invoked by the @{command "case"} command.
@@ -1157,10 +1156,10 @@
\<^medskip>
\begin{tabular}{llll}
- facts & & arguments & rule \\\hline
- & @{method induct} & \<open>P x\<close> & datatype induction (type of \<open>x\<close>) \\
+ facts & & arguments & rule \\\hline
+ & @{method induct} & \<open>P x\<close> & datatype induction (type of \<open>x\<close>) \\
\<open>\<turnstile> A x\<close> & @{method induct} & \<open>\<dots>\<close> & predicate/set induction (of \<open>A\<close>) \\
- \<open>\<dots>\<close> & @{method induct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
+ \<open>\<dots>\<close> & @{method induct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
\end{tabular}
\<^medskip>
@@ -1176,9 +1175,9 @@
the induction rule. Equalities reappear in the inductive cases, but have
been transformed according to the induction principle being involved here.
In order to achieve practically useful induction hypotheses, some variables
- occurring in \<open>t\<close> need to be fixed (see below). Instantiations of the form
- \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a shorthand for \<open>x \<equiv> t\<close>,
- where \<open>x\<close> is a fresh variable. If this is not intended, \<open>t\<close> has to be
+ occurring in \<open>t\<close> need to generalized (see below). Instantiations of
+ the form \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a shorthand for \<open>x \<equiv>
+ t\<close>, where \<open>x\<close> is a fresh variable. If this is not intended, \<open>t\<close> has to be
enclosed in parentheses. By default, the equalities generated by
definitional instantiations are pre-simplified using a specific set of
rules, usually consisting of distinctness and injectivity theorems for
@@ -1205,8 +1204,8 @@
\<^medskip>
\begin{tabular}{llll}
- goal & & arguments & rule \\\hline
- & @{method coinduct} & \<open>x\<close> & type coinduction (type of \<open>x\<close>) \\
+ goal & & arguments & rule \\\hline
+ & @{method coinduct} & \<open>x\<close> & type coinduction (type of \<open>x\<close>) \\
\<open>A x\<close> & @{method coinduct} & \<open>\<dots>\<close> & predicate/set coinduction (of \<open>A\<close>) \\
\<open>\<dots>\<close> & @{method coinduct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
\end{tabular}