author nipkow Thu, 01 Feb 1996 16:18:52 +0100 changeset 1471 b088c0a1f2bd parent 1470 49b3e075f124 child 1472 a89803e3d1bd
documented split_all_tac in HOL.
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions
--- 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