Author: Daniel Winterstein
Title: Proof General / Eclipse - A generic interface for interactive theorem provers
Abstract: 
Good interfaces and development tools are crucial if interactive proof 
systems are to be adopted by mathematicains and computer programmers. 
Unfortunately, the development tools available for theorem provers are 
often quite rudimentary. The Proof General project is an ongoing attempt 
to redress this. PG/Eclipse marks an exciting new phase in the project. 
The new interface is not only much prettier than the old Emacs based 
system, but also offers more sophisticated functionality. It is built 
using a protocol for interactive proof sessions called PGIP, and will 
work with any prover that implements this protocol. Currently, that 
means the latest version of Isabelle - but hopefully it will be 
relatively easy to adapt any interactive prover to use PGIP. Lucas Dixon 
will be demonstrating the software, showing off some new features and a 
wide range of bugs.