# HG changeset patch
# User nipkow
# Date 823187932 -3600
# Node ID b088c0a1f2bd5b12e0c0c5470feb46dffe9f512d
# Parent  49b3e075f124a9ed67068a888c9405011a878c8b
documented split_all_tac in HOL.

diff -r 49b3e075f124 -r b088c0a1f2bd doc-src/Logics/HOL.tex
--- a/doc-src/Logics/HOL.tex	Thu Feb 01 13:25:40 1996 +0100
+++ b/doc-src/Logics/HOL.tex	Thu Feb 01 16:18:52 1996 +0100
@@ -973,8 +973,18 @@
 \item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}
 \item[Sets:] {\tt \{~{\it pattern}~.~$P$~\}}
 \end{description}
-% FIXME: remove comment in HOL/Prod.thy concerning printing
-% FIXME: remove ML code from HOL/Prod.thy
+
+There is a simple tactic which supports reasoning about patterns:
+\begin{ttdescription}
+\item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all
+  {\tt!!}-quantified variables of product type by individual variables for
+  each component. A simple example:
+\begin{ttbox}
+{\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}
+by(split_all_tac 1);
+{\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}
+\end{ttbox}
+\end{ttdescription}
 
 Theory {\tt Prod} also introduces the degenerate product type {\tt unit}
 which contains only a single element named {\tt()} with the property