Proof General Eclipse User Documentation

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.

Installation

1. Download and install a modern version of Isabelle
2. Download Proof General / Eclipse - see PGEclipseInstall
3. Install Proof General / Eclipse - see PGEclipseInstall
4. Start Proof General / Eclipse using the ''eclipse'' binary
5. New to Isabelle? See our PGEclipseIsabelleTutorial [*NB* presently outdated]

See PGEclipseInstall. For trouble-shooting, see PGEclipseInstallProbs.

Basic Ideas

Please see InterfaceConcepts, PGEclipseGettingStarted or PGEclipseTasks.

Symbol support

PG Eclipse supports the use of mathematical symbols. See PGEclipseSymbolTableEditor for more information.

Teacher View

The Teacher View is a web browser for viewing tutorials that link to Proof General. These can activate certain functions within Proof General (either by linking to a .thy file or by Javascript).

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.