The forefather of Proof General was LEGO mode, begun by Thomas Kleymann in 1994 as an Emacs-based front end for LEGO similar to Isamode. Later, implementations of proof-by-pointing and script management were added, and the code was made generic.
This generic basis for Proof General was developed at the LFCS by Kleymann, Sequeira, Goguen and Aspinall (in order of appearance). Early on, Yves Bertot provided assistance, and Proof General follows some of the ideas used in Project CROAP. The authors and current maintainers of the various instantiations of Proof General are mentioned on the
The Proof General project was coordinated until October 1998 by Thomas Kleymann, and since then by David Aspinall. The project has benefited from funding by EPSRC and the EC.
David Aspinall designed the web pages and graphics for Proof General.
Check the gallery for more publicity
pictures!
For more on the history of the development of the Proof General program, see the
Have you any questions, comments, or suggestions about Proof General?
Send us a message using this form.
Discuss Proof General with other users and receive announcements by joining our mailing list.