documented split_all_tac in HOL.
Thu, 01 Feb 1996 16:18:52 +0100
changeset 1471 b088c0a1f2bd
parent 1470 49b3e075f124
child 1472 a89803e3d1bd
documented split_all_tac in HOL.
--- 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$~\}}
-% 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:
+\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:
+{\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)}
 Theory {\tt Prod} also introduces the degenerate product type {\tt unit}
 which contains only a single element named {\tt()} with the property