# HG changeset patch
# User wenzelm
# Date 959354947 -7200
# Node ID 4e55d773d0185f7a003ae223dd660a58bc574c62
# Parent  802acc97fdaf528f8cbe7e65e691e62a164630f0
tuned case_tac;

diff -r 802acc97fdaf -r 4e55d773d018 doc-src/IsarRef/hol.tex
--- 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}