--- a/doc-src/Ref/classical.tex Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/classical.tex Thu Nov 27 19:39:02 1997 +0100
@@ -446,7 +446,7 @@
proof using \texttt{blast_tac} can be made much faster by supplying the
successful search bound to this tactic instead.
-\item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover}
+\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
causes the tableau prover to print a trace of its search. At each step it
displays the formula currently being examined and reports whether the branch
has been closed, extended or split.