# HG changeset patch
# User wenzelm
# Date 1619862849 -7200
# Node ID f28df88c0d006c21e25b149ac7a66bde9be90be4
# Parent  cc36841eeff6b25b72ade1e08879c630cc377738
tuned;

diff -r cc36841eeff6 -r f28df88c0d00 src/Doc/Isar_Ref/Proof.thy
--- 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}