# HG changeset patch
# User nipkow
# Date 861901712 -7200
# Node ID 4ef28e05781beba39a6e316fff16453ec6ca946d
# Parent  3e3087aa69e7c4888c169615f9a918eb8d3e0736
Added 'induct_tac'

diff -r 3e3087aa69e7 -r 4ef28e05781b doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Thu Apr 24 18:51:14 1997 +0200
+++ b/doc-src/Logics/HOL.tex	Thu Apr 24 19:08:32 1997 +0200
@@ -1110,7 +1110,7 @@
 \subcaption{Constants and infixes}
 
 \begin{ttbox}\makeatother
-\tdx{nat_induct}     [| P 0; !!k. [| P k |] ==> P(Suc k) |]  ==> P n
+\tdx{nat_induct}     [| P 0; !!n. P n ==> P(Suc n) |]  ==> P n
 
 \tdx{Suc_not_Zero}   Suc m ~= 0
 \tdx{inj_Suc}        inj Suc
@@ -1223,9 +1223,9 @@
 %The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
 %natural numbers are most easily expressed using recursion along~$<$.
 
-The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
-variable~$n$ in subgoal~$i$ using theorem {\tt nat_induct}. There is also the
-derived theorem \tdx{less_induct}
+Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
+in subgoal~$i$ using theorem {\tt nat_induct}. There is also the derived
+theorem \tdx{less_induct}
 \begin{ttbox}
 [| !!n. [| ! m. m<n --> P m |] ==> P n |]  ==>  P n
 \end{ttbox}
@@ -1368,9 +1368,9 @@
 
 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
 operations with their types and syntax. The type constructor {\tt list} is
-defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}.  This
-yields an induction tactic {\tt list.induct_tac} of type {\tt string -> int
--> tactic}. A \sdx{case} construct of the form
+defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}.  As a
+result the generic induction tactic \ttindex{induct_tac} also performs
+structural induction over lists. A \sdx{case} construct of the form
 \begin{center}\tt
 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b
 \end{center}
@@ -1617,11 +1617,11 @@
 
 Most of the theorems about the datatype become part of the default simpset
 and you never need to see them again because the simplifier applies them
-automatically. Only induction is invoked by hand. Loading a theory containing
-a datatype $t$ defines $t${\tt.induct_tac}:
+automatically. Only induction is invoked by hand:
 \begin{ttdescription}
-\item[$t$.\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
- applies structural induction over variable $x$ to subgoal $i$.
+\item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]
+ applies structural induction on variable $x$ to subgoal $i$, provided the
+ type of $x$ is a datatype or type {\tt nat}.
 \end{ttdescription}
 
 For the technically minded, we give a more detailed description.
@@ -1665,7 +1665,7 @@
 \end{ttbox}
 This can be proved by the structural induction tactic:
 \begin{ttbox}
-by (MyList.list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 {\out Level 1}
 {\out ! x. Cons x xs ~= xs}
 {\out  1. ! x. Cons x Nil ~= Nil}
@@ -1824,7 +1824,7 @@
 leads to short proofs:
 \begin{ttbox}\underscoreon
 goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
-by (MyList.list.induct\_tac "xs" 1);
+by (induct\_tac "xs" 1);
 by (ALLGOALS Asm\_simp\_tac);
 \end{ttbox}