Welcome to I3P I3P Logo

I3P is an Interactive Interface for the Isabelle Prover. The two goals of the I3P development are interactivity and extensibility: users should be able to interact with an interactive theorem prover in more ways than executing and undoing commands, and they should be able to add in well-defined ways specific user-interface functionality to support them in their specific projects.

To simplify the transition, I3P emulates the behaviour of the Emacs-based ProofGeneral: as the main difference, the keyboard shortcuts replace Ctrl-C by Ctrl-Shift. The software structure is designed to support the given project goals - feel free to have a look at a snapshot of the sources.

Installation: Download the application, unzip the archive, and start i3p/bin/i3p. I3P has been tested on Linux, MacOS, and Windows/Cygwin.

Repository access The sources are available in the repository (user&password: anon)

            hg clone https://subversion.informatik.uni-tuebingen.de/hg/i3p
The releases are tagged.


10.6.2012:Updated driver for Isabelle2012

22.2.2012: Added module APIAccess which provides a simple facade for driving Isabelle in the background.

Since the change does not concern the existing infrastructure, no new release has been compiled. The source code is available from the above repository.

20.10.2011: The release 1.0.11 includes the tested Isabelle2011-1 driver.

Note: Due to an upgrade to Netbeans 7.0, you may have to delete .i3p in your home directory.

31.1.2011: The release 1.0.10 includes the tested Isabelle2011 driver. A new source snapshot is available.

10.12.10: The release 1.0.9 improves Cygwin support with a special installation type and starts adaptation for the upcoming Isabelle 2010 release. A new source snapshot is available.

5.10.10: The release 1.0.8 introduces lazy printing of goal states, which significantly speeds up theory processing. A new source snapshot is available.

13.8.10: The release 1.0.7 adds support for sledgehammer.

2.8.10: The release 1.0.6 adds Toolbar buttons for next/undo/goto point.

22.7.10: The release 1.0.5 automatic pre-installation of the IsabelleText font.

22.7.10: The font support module, which provides the XSymbol encoding and decoding, with a bundled IsabelleText font from the Isabelle distribution, is available standalone: The JAR file can just be linked to a Swing-based application. To try the functionality, just run

	  java -cp org-i3p-fontsupport.jar org.i3p.fontsupport.demo.SymbolPaneDemo
The sources also provide documentation.

20.7.10: The release 1.0.4 adds auto-completion for XSymbol entry and automatic pre-installation of the IsabelleText font.

Contact: I3P was written by Holger Gast. He's very grateful for any feedback, so feel free to send an email.

Some features that distinguish I3P are the following: