Abstract: Proof General meets IsaWin

Proof General meets IsaWin
Combining Text-Based And Graphical User Interfaces

David Aspinall
University of Edinburgh, Department of Computer Science

Christoph Lüth
FB 3 - Mathematik und Informatik, Universität Bremen

We describe the design and prototype implementation of a combination of theorem prover interface technologies. On one side, we take from Proof General the idea of a prover-independent interaction language and its proposed implementation within the PG Kit middleware architecture. On the other side, we take from IsaWin a sophisticated graphical metaphor using direct manipulation for developing proofs. We believe that the resulting system will provide a powerful, robust and generic environment for developing proofs within interactive proof assistants that also opens the way for studying and implementing new mechanisms for managing interactive proof development.

Christoph Lüth, 23.06.04