[isabelle] Isabelle/Eclipse prover IDE released!

Dear Isabelle users,

I am pleased to announce the first _official_ release of Isabelle/Eclipse!

Isabelle/Eclipse provides an Eclipse integration for Isabelle, based on
Isabelle/Scala. It started as a port of Isabelle/jEdit to integrate with
Eclipse IDE. Today Isabelle/Eclipse is available as a standalone prover
IDE, as well as plug-ins for integration with Eclipse IDE of your choice.

Learn more about Isabelle/Eclipse and download it from its website:


In many ways Isabelle/Eclipse mirrors Isabelle/jEdit, but aims to provide
Eclipse-native functionality to use Isabelle. 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. Learn more about
Isabelle/Eclipse features on the website. Check out the list of closed
issues to see what has been implemented and fixed in this release:


Before you start Isabelle/Eclipse, I advise reading the "Getting started"
page on the website. Also make sure you are using Java 7 and Isabelle 2013.

# Reporting issues & contributing

Note that Isabelle/Eclipse still has several known issues, notably no
support for sub/super-script, bold and other control symbols, as well as
lack of nice UI to configure certain Isabelle options. You can view all
open issues for Isabelle/Eclipse here:


Please report any bugs, feature requests, questions and other issues you
encounter using the link above - I will appreciate your input!

Isabelle/Eclipse is open-source and the source code is available on GitHub:


I welcome all contributions and help - if you see an open issue that you
want to hack at, feel free to!

Isabelle/Eclipse started as an attempt to get Isabelle working from within
Eclipse IDE. There are a number of formal methods tools building on the
Eclipse platform and I hope that Isabelle/Eclipse will be useful to
integrate them with the Isabelle theorem prover.

Great thanks to Makarius for his assistance, input and all the work on
Isabelle and Isabelle/Scala.

Let me know what you think!

Best regards,
Andrius Velykis
Newcastle University / AI4FM project

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.