1: \begin{definition}[

2: A \emph{Target Theorem (TT)} is a theorem currently being attempted in

3:   ACL2, but requiring user's intervention. 

4: A \emph{Source Theorem (ST)} is a theorem which has been suggested as similar to the TT

5:   by the statistical ACL2(ml).

6: %\end{definition}

7: