doc-src/Ref/classical.tex

 
 \item[\ttindexbold{sizef}] is the heuristic function used for best-first
 search.  It should estimate the size of the remaining subgoals.  A good
 heuristic function is \ttindex{size_of_thm}, which measures the size of the
 proof state.  Another size function might ignore certain subgoals (say,
-those concerned with type checking).  A heuristic function might simply
+those concerned with type-checking).  A heuristic function might simply
 count the subgoals.
 
 \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in
 the hypotheses, typically created by \ttindex{HypsubstFun} (see
 Chapter~\ref{substitution}).  This list can, of course, be empty.  The