tuned;
authorwenzelm
Sat, 01 May 2021 11:54:09 +0200
changeset 73868 f28df88c0d00
parent 73867 cc36841eeff6
child 73869 c1d8cd6d1a49
tuned;
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}