Documentation is sadly lacking at present. Please request help on unclear areas (edit this page, adding your question), or contribute to this document by adding some hints you think may be useful.
See PGEclipseInstall. For trouble-shooting, see PGEclipseInstallProbs.
Please see InterfaceConcepts, PGEclipseGettingStarted or PGEclipseTasks.
PG Eclipse supports the use of mathematical symbols. See PGEclipseSymbolTableEditor for more information.
It is activated via the Proof General menu.
For an example, open this web page in PG/E, then try clicking here: http://www.inf.ed.ac.uk/teaching/courses/ar/slides/sample.thy This should open a sample .thy file, which can then be edited or run.
We have written an PGEclipseIsabelleTutorial for use with this view. (Unfortunately it's currently out of date and broken, please fix if you are interested in it).
If you are interested in using the Teacher View, please see the ed.inf.proofgeneral.welcome project (available only in CVS at present) for an example.