with the system, but she can experiment with variations of the proof given
in the tutorial as much as she like, still getting useful suggestions.
Thus the user is allowed to focus on learning how to do a formal proof
instead of wasting efforts trying to remember the interface to the system.
\item{Tutors for Computationally Expensive Tactics}. Several tactics have
with the system, but she can experiment with variations of the proof given
in the tutorial as much as she like, still getting useful suggestions.
Thus the user is allowed to focus on learning how to do a formal proof
instead of wasting efforts trying to remember the interface to the system.
\item{Tutors for Computationally Expensive Tactics}. Several tactics have