doc-src/Ref/tctical.tex
changeset 4317 7264fa2ff2ec
parent 3108 335efc3f5632
child 5371 e27558a68b8d
--- a/doc-src/Ref/tctical.tex	Thu Nov 27 19:37:36 1997 +0100
+++ b/doc-src/Ref/tctical.tex	Thu Nov 27 19:39:02 1997 +0100
@@ -96,7 +96,7 @@
 is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at
 least once, failing if this is impossible.
 
-\item[\ttindexbold{trace_REPEAT} := true;] 
+\item[set \ttindexbold{trace_REPEAT};] 
 enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM}
 and {\tt REPEAT}.  To view the tracing options, type {\tt h} at the prompt.
 \end{ttdescription}
@@ -202,7 +202,7 @@
 uses {\tt DEPTH_FIRST} to search for states having fewer subgoals than the
 given state.  Thus, it insists upon solving at least one subgoal.
 
-\item[\ttindexbold{trace_DEPTH_FIRST} := true;] 
+\item[set \ttindexbold{trace_DEPTH_FIRST};] 
 enables interactive tracing for {\tt DEPTH_FIRST}.  To view the
 tracing options, type {\tt h} at the prompt.
 \end{ttdescription}
@@ -242,7 +242,7 @@
 contains the result of applying $tac@0$ to the proof state.  This tactical
 permits separate tactics for starting the search and continuing the search.
 
-\item[\ttindexbold{trace_BEST_FIRST} := true;] 
+\item[set \ttindexbold{trace_BEST_FIRST};] 
 enables an interactive tracing mode for the tactical {\tt BEST_FIRST}.  To
 view the tracing options, type {\tt h} at the prompt.
 \end{ttdescription}
@@ -289,11 +289,11 @@
 \hbox{\tt has_fewer_prems $n$} is a predicate on theorems; it may 
 be given to the searching tacticals.
 
-\item[\ttindexbold{eq_thm}($thm1$,$thm2$)] 
-reports whether $thm1$ and $thm2$ are equal.  Both theorems must have
-identical signatures.  Both theorems must have the same conclusions, and
-the same hypotheses, in the same order.  Names of bound variables are
-ignored.
+\item[\ttindexbold{eq_thm} ($thm_1$, $thm_2$)] reports whether $thm_1$
+  and $thm_2$ are equal.  Both theorems must have identical
+  signatures.  Both theorems must have the same conclusions, and the
+  same hypotheses, in the same order.  Names of bound variables are
+  ignored.
 
 \item[\ttindexbold{size_of_thm} $thm$] 
 computes the size of $thm$, namely the number of variables, constants and