--- 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}