Organize your proof with Emacs! Home Screenshot Download Documentation

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.