# HG changeset patch
# User wenzelm
# Date 953574185 -3600
# Node ID 54acec31dcacd1fd399b8d39c46471010a2f031f
# Parent  ed6962a0763f9c5acde4b12758f1f0b08242f647
case_tac, induct_tac;

diff -r ed6962a0763f -r 54acec31dcac doc-src/IsarRef/hol.tex
--- a/doc-src/IsarRef/hol.tex	Mon Mar 20 18:42:50 2000 +0100
+++ b/doc-src/IsarRef/hol.tex	Mon Mar 20 18:43:05 2000 +0100
@@ -111,7 +111,11 @@
 
 See \cite{isabelle-HOL} for more details on datatypes.  Note that the theory
 syntax above has been slightly simplified over the old version, usually
-requiring more quotes and less parentheses.
+requiring more quotes and less parentheses.  Apart from proper proof methods
+for case-analysis and induction, there are also emulations of ML tactics
+\texttt{case_tac}\indexisarmeth{case-tac} and
+\texttt{induct_tac}\indexisarmeth{induct-tac} available, with similar syntax
+as $subgoal_tac$, see \S\ref{sec:tactical-proof}.
 
 
 \section{Recursive functions}