-
-
-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 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!
-
-