Eclipse integration for Isabelle proof assistant

Support for Isabelle2013-1

Isabelle/Eclipse does not support Isabelle2013-1 at the moment. The upgrade to support the new version is planned. Unfortunately, due to writing-up of my PhD thesis, the upgrade is likely to be delayed until early next year.


Eclipse plug-ins that provide Prover IDE for Isabelle proof assistant, based on Isabelle/Scala framework.

Isabelle/Eclipse started as a port of Isabelle/jEdit Prover IDE to integrate with Eclipse IDE as plug-ins. The integration uses common Eclipse components to provide theory editing, correct symbols, completion assistance, prover output and other features. By building on Eclipse it inherits various IDE goodies out of the box.


Getting started

To use Isabelle/Eclipse, download it either as standalone Isabelle/Eclipse IDE or use the update site to install the plug-ins into your Eclipse. The latest Isabelle/Eclipse requires Java 7 to run and works with Isabelle 2013 only. Refer to the Downloads page for download links and further details.

After downloading/installing Isabelle/Eclipse, open Isabelle perspective, create projects for your Isabelle theory files, launch the Isabelle prover and start proving! Read more about the first steps in the Getting started page.


Isabelle/Eclipse provides a familiar Eclipse-based prover IDE with numerous features. Read about some of the features here.


Please report bugs, feature requests, questions and other issues using the GitHub tracker:

You can also contribute to the project by forking the repository and sending pull requests with your changes. We welcome various contributions!

Isabelle/Eclipse is built on Eclipse platform using Scala and Java programming languages. It is built using Maven and Eclipse Tycho. Refer to the Developer documentation for hints on building Isabelle/Eclipse yourself.

Feel free to contact the author for assistance.


Developed by Andrius Velykis (Newcastle University, UK) as part of the AI4FM research project.