doc-src/Ref/classical.tex
changeset 4317 7264fa2ff2ec
parent 3720 a5b9e0ade194
child 4398 6c5d61fd3379
     1.1 --- a/doc-src/Ref/classical.tex	Thu Nov 27 19:37:36 1997 +0100
     1.2 +++ b/doc-src/Ref/classical.tex	Thu Nov 27 19:39:02 1997 +0100
     1.3 @@ -446,7 +446,7 @@
     1.4    proof using \texttt{blast_tac} can be made much faster by supplying the
     1.5    successful search bound to this tactic instead.
     1.6    
     1.7 -\item[\ttindexbold{Blast.trace} := true;] \index{tracing!of classical prover}
     1.8 +\item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover}
     1.9    causes the tableau prover to print a trace of its search.  At each step it
    1.10    displays the formula currently being examined and reports whether the branch
    1.11    has been closed, extended or split.