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.David Aspinall and Christoph Lüth. Proof General meets IsaWin.
Click here to return to my papers page.