+
+
+Building a simple proof in LEGO with proof-by-pointing.
+
+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
+X-Symbol
+package in conjunction with Proof General.
+Here you can see some symbols in Isabelle's output.
+
+
++Replaying a proof in Isar, Isabelle's new 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!
+