# HG changeset patch
# User wenzelm
# Date 1213118116 -7200
# Node ID 11fcdd5897dd1294750658ea4c672b77c9d7a48d
# Parent  63d92a5e3784dd83ad0473fcb01fade481d97ff4
case_tac/induct_tac: use same declarations as cases/induct;

diff -r 63d92a5e3784 -r 11fcdd5897dd doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jun 10 19:15:14 2008 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Jun 10 19:15:16 2008 +0200
@@ -773,17 +773,18 @@
 *}
 
 
-section {* Cases and induction: emulating tactic scripts \label{sec:hol-induct-tac} *}
+section {* Unstructured cases analysis and induction \label{sec:hol-induct-tac} *}
 
 text {*
-  The following important tactical tools of Isabelle/HOL have been
-  ported to Isar.  These should be never used in proper proof texts!
+  The following tools of Isabelle/HOL support cases analysis and
+  induction in unstructured tactic scripts; see also
+  \secref{sec:cases-induct} for proper Isar versions of similar ideas.
 
   \begin{matharray}{rcl}
     @{method_def (HOL) case_tac}@{text "\<^sup>*"} & : & \isarmeth \\
     @{method_def (HOL) induct_tac}@{text "\<^sup>*"} & : & \isarmeth \\
     @{method_def (HOL) ind_cases}@{text "\<^sup>*"} & : & \isarmeth \\
-    @{command_def (HOL) "inductive_cases"} & : & \isartrans{theory}{theory} \\
+    @{command_def (HOL) "inductive_cases"}@{text "\<^sup>*"} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
   \begin{rail}
@@ -803,14 +804,18 @@
   \begin{descr}
 
   \item [@{method (HOL) case_tac} and @{method (HOL) induct_tac}]
-  admit to reason about inductive datatypes only (unless an
-  alternative rule is given explicitly).  Furthermore, @{method (HOL)
-  case_tac} does a classical case split on booleans; @{method (HOL)
-  induct_tac} allows only variables to be given as instantiation.
-  These tactic emulations feature both goal addressing and dynamic
+  admit to reason about inductive types.  Rules are selected according
+  to the declarations by the @{attribute cases} and @{attribute
+  induct} attributes, cf.\ \secref{sec:cases-induct}.  The @{command
+  (HOL) datatype} package already takes care of this.
+
+  These unstructured tactics feature both goal addressing and dynamic
   instantiation.  Note that named rule cases are \emph{not} provided
-  as would be by the proper @{method induct} and @{method cases} proof
-  methods (see \secref{sec:cases-induct}).
+  as would be by the proper @{method cases} and @{method induct} proof
+  methods (see \secref{sec:cases-induct}).  Unlike the @{method
+  induct} method, @{method induct_tac} does not handle structured rule
+  statements, only the compact object-logic conclusion of the subgoal
+  being addressed.
   
   \item [@{method (HOL) ind_cases} and @{command (HOL)
   "inductive_cases"}] provide an interface to the internal @{ML_text