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
- Download and install a modern version of Isabelle
- Download Proof General / Eclipse - see PGEclipseInstall
- Install Proof General / Eclipse - see PGEclipseInstall
- Start Proof General / Eclipse using the ''eclipse'' binary
- 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.
Main.PGEclipseUserDocumentation moved from Main.PGEclipseUserDoc on 23 Aug 2006 - 23:44 by DavidAspinall