A New Interface for HOL – Ideas, Issues and Implementation

TkHolWorkbench is a new set of interface tools for HOL implemented using the Tk toolkit. It aims to be robust, extensible, lightweight and user-friendly. The tools are designed to augment the existing HOL interface. The project applies rapid prototyping and the use of an interpreted toolkit to the field of theorem proving interfaces. The topics considered in this paper are: the motivations for a new interface for HOL; the design objectives and usability targets for TkHolWorkbench; a description of the TkHolWorkbench tools as they now stand; and the extensible design architecture used in the implementation.