--- a/doc-src/Ref/tactic.tex Mon Oct 20 11:47:04 1997 +0200
+++ b/doc-src/Ref/tactic.tex Mon Oct 20 11:53:42 1997 +0200
@@ -7,8 +7,8 @@
expressed using basic tactics and tacticals.
This chapter only presents the primitive tactics. Substantial proofs require
-the power of simplification (Chapter~\ref{simp-chap}) and classical reasoning
-(Chapter~\ref{chap:classical}).
+the power of simplification (Chapter~\ref{chap:simplification}) and classical
+reasoning (Chapter~\ref{chap:classical}).
\section{Resolution and assumption tactics}
{\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using