  We describe a prototype theorem prover, UTP2, developed to match the style of
hand-written proof work in the Unifying Theories of Programming semantical
framework. This is based on alphabetised predicates in a 2nd-order logic, with
a strong emphasis on equational reasoning. We present here an overview of the
user-interface of this prover, which was developed from the outset using a
point-and-click approach. We contrast this with the command-line paradigm that
continues to dominate the mainstream theorem provers, and raises the question:
can we have the best of both worlds?
