author wenzelm Fri, 26 May 2000 17:29:07 +0200 changeset 8980 4e55d773d018 parent 8979 802acc97fdaf child 8981 fe1f3d52e027
tuned case_tac;
 doc-src/IsarRef/hol.tex file | annotate | diff | comparison | revisions
--- a/doc-src/IsarRef/hol.tex	Fri May 26 11:18:06 2000 +0200
+++ b/doc-src/IsarRef/hol.tex	Fri May 26 17:29:07 2000 +0200
@@ -349,11 +349,12 @@
;
\end{rail}

-By default, $case_tac$ and $induct_tac$ admit to reason about datatypes only,
-unless an alternative explicit rule is given; only variables may be given as
-instantiation for $induct_tac$.  Also note that named local contexts (see
-\S\ref{sec:cases}) are not provided as would be by the proper $induct$ and
-$cases$ proof methods (see \S\ref{sec:induct-method-proper}).
+By default, $case_tac$ and $induct_tac$ admit to reason about inductive
+datatypes only, unless an alternative rule is given explicitly.  Furthermore,
+$case_tac$ does a classical case split on booleans; $induct_tac$ allows only
+variables to be given as instantiation.  Also note that named local contexts
+(see \S\ref{sec:cases}) are not provided as would be by the proper $induct$
+and $cases$ proof methods (see \S\ref{sec:induct-method-proper}).

\section{Arithmetic}