Isabelle Add-On Tools and Components
- linter: An Isabelle/Isar linter.
- 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.