
Building a simple proof in LEGO with proofbypointing.
The top half of the window displays the proof script.
The bottom displays the output from LEGO at each
stage of the proof. Here, it shows
the current subgoals to be solved.
The part of the proof already processed by LEGO
has a blue background.
Clicking on terms in the subgoals list generates
commands which are added to the proof script.


Coq Proof General running in multiple frame mode,
full screen shot (1024x768).
There are separate windows on the screen
for the script, goals, and response buffers.
In this picture, you can see Proof General's
indication that Coq is processing the
induction step, because the background of
the proof step is pink. It will become
blue when Coq finishes that step.


Replaying a domain theory proof in Isabelle's HOLCF logic.
In Isabelle, theory files as well as ML files are coloured.
Proof General has some functions for processing and
undoing theory files, but most operations it provides
are for writing proof scripts in ML files.
Isabelle supports input and output in tokens which
display as symbols using the
XSymbol
package in conjunction with Proof General.
Here you can see some symbols in Isabelle's output.


Replaying a proof in Isar, Isabelle's declarative proof language
developed by Markus Wenzel.


LEGO Proof General running in plain console mode.
This shows that you can run Proof General even if sometimes
you need to use a plain tty or xterminal. Of course, the
graphical features are reduced!
