Interactive theorem proving benefits from graphical user interfaces: visualization of concepts helps non-experts to cope with the involved complexity, while experts can automate frequent tasks.
In an ongoing project to provide a usable interface for the Isabelle prover, the following steps have been accomplished.