Proof General --- Organize your proof with Emacs

Organize your proof with Emacs!

This is a picture of Isabelle Proof General running inside XEmacs, replaying a simple proof.
The top half of the window displays the proof script.
The blue highlighted region is the part of the script which has been sent to the proof process so far. It cannot be edited.
The bottom half of the window displays the output from Isabelle at each stage of the proof.

Isabelle Proof General screenshot

Proof General maintainer

Last modified: Fri Oct 9 14:22:02 BST 1998