Screenshot notes.
=================

All in 80x40 sized XEmacs.  

* Isabelle: Dagstuhl HOLCF example.  Show theory file on screen too.

* Isar: Example Group.thy is modified version with extra X-Symbol line:

syntax (xsymbols)
  "op *"      :: "['a::times, 'a] => 'a"          (infixl "\\<bullet>" 70);

And uses of * replaced with \\<bullet>.

* Coq: Example from Sorting library.  Multiple frame mode, X-Symbols,
also with Netscape.  

Most shots scaled to 0.2 or thereabouts to give nice sized thumbnail.






-----------------------------------------------------------------

Regenerating screen shot in html/IsaPGscreen.jpg:

 30x80 sized XEmacs.  Visit isa/example.ML.
 Click on "next" button four times. 
 Drag middle modeline to display whole proof script.
 Move point to end of locked region.
 Grab with gimp, Xtns -> Screen Shot.
 Save with default quality settings.

-----------------------------------------------------------------