Isabelle Add-On Tools and Components

Quick link: isabelle.systems/addons/<code>, e.g. isabelle.systems/addons/linter

Isabelle/jEdit

• linter: An Isabelle/Isar linter.

Outdated

• awe: Provides facilities to establish morphisms between theories, allowing the interpretation of logical entities from one theory to another.
• hol-ocl: Interactive proof environment for the Object Constraint Language (OCL).
• hol-testgen: Environment for model-based Test-Generation. Models for unit-, sequence and reactive-sequence test scenarios can be written in HOL and tests are generated automatically.
• i3p: Interactive Interface for Isabelle.