Isabelle with Proof General Eclipse: An Overview and User Introduction

David Aspinall, Christoph Lüth

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We give a user-oriented presentation of the new Proof General Eclipse interface for Isabelle and a brief demonstration of its use. We also provide some background information and remarks about the implementation. This new version of Proof General will bring the features of a industrial-strength IDE to theorem proving for the first time. The first version implements the standard script management metaphor which is known from the existing Proof General system, to offer a familiar upgrade path. Future versions will extend and improve script management in several ways. Features of the first version include: • an outline view showing the structure of the proof text, allowing easy navigation and reflecting the state of the checking progress; • folding within proof scripts, allowing regions to be contracted/expanded; • information hovers, displaying, e.g., theorems or the proofstate; • content assistance, providing identifier completion and proof fragment templates; • error (and information, warning) markers attached to proof text; • a history of previous proofstates and other outputs; • a navigator for files in a proof project, which decorates proof scripts according to their status within the current session; • a theory browser, exploring theories and theorems available in the current session; • symbol handling for input and output using Unicode fonts (promising high-quality rendering once the Stixfonts project is complete) and CSS transformations; • fully flexible layout of windows on the workspace or desktop; • other workbench features provided by Eclipse and further plugins, such as bookmarks, textual searching, version control support, a LATEX editor, etc. One of the motivations for our presentation is to solicit feedback and suggestions for the interface, and to point out the opportunities for collaboration. Further development will be required before the system is ready for mainstream use, so at the present moment there is a chance to affect the final system. Credits. Proof General Eclipse has been developed by Daniel Winterstein, Alex Heneveld, David Aspinall, and Graham Dutton. It uses the Proof General Kit framework and PGIP protocol designed by Aspinall and L¨uth.
Original languageEnglish
Title of host publicationCADE-21 The 21st Conference on Automated Deduction
Subtitle of host publicationThe Isabelle Workshop 2007
Number of pages1
Publication statusPublished - 2007


Dive into the research topics of 'Isabelle with Proof General Eclipse: An Overview and User Introduction'. Together they form a unique fingerprint.

Cite this