TkHol was an experimental theorem prover interface for the HOL system. TkHOL is no longer maintained. It's emphasis was on usability and end-user interaction. The user activity supported was "theory development", which means that TkHol was a tool which helps the user perform the activities which go into constructing the development of HOL theories and proofs.
The following screen shotsshow two examples of TkHol in action. I believe the main contribution of TkHOL was to take seriously the notion of proof debugging, i.e. to explicitly use a GUI to support the process of getting rid of mistakes in existing proofs, based around a conceptual model similar to existing step-through debuggers.
Developing theorem prover interfaces is difficult - interfaces for symbolic systems have their own difficulties, and in many cases we don't even begin to know what a good interface for such a system would look like (or, indeed, what a really good theorem proving system would look like at all). It involves trying to develop an interface for a highly structured, logical problem that requires very precise expression of a solution, i.e. trying to make something that is inherently very hard, even on paper, just that little bit easier by using a machine.
TkHol 0.3 is still available from the Cambridge ftp site. The README for that release is also available.
TkHol was implemented using the Tk/Tcl toolkit.
After finishing my work on TkHol and gaining experience via user feedback, I went on to develop DECLARE, which used a very different and limited style of proof, and one which I believe was much more suited to graphical presentation.
I used TkHol to explore the issues involved in delivering advanced interaction to all kinds of users of theorem provers. I considered user involvement in this process extremely important, but also realised that users won't become involved unless they are given something which actually works. Theorem prover users still typically interact with the theorem prover via a command line interfaces. These are great for programming tasks but not much else. For instance, they deliver little in terms of visualisation support. This is an obvious way in which graphical tools can boost the power of theorem proving systems.
The following people, who used to share an office with me, were the most regular users of TkHol. They were exceptionally helpful with providing user feedback.
Throughout the development of TkHol I found input from the field Human Computer Interaction (HCI) useful. A group at Glasgow were doing similar work, also with a particular emphasis on HCI aspects of theorem proving, though with less emphasis on implementation. More than anything else I have found that HCI gives a vocabulary for talking about all the weird complications that arise when designing a user interface. A good vocabulary is particularly helpful when analysing the user activity that the interface is meant to support. Also, HCI studies continually remind us of the importance of usability and the user's mental model of what's going on. I found the book Interactive Systems, (Newman and Lamming, Addison Wesley 1995) extremely helpful.
Several previous attempts were made to implement an interface for HOL. CHOL by Laurent Thery is the most significant of these. Note also Tom Schubert's xhol and Sara Kalvala's unnamed interface work.