Owner: makarius

Category: Application

Isabelle theorem prover

Isabelle is a theorem prover for higher-order logics (HOL, ZF etc.). It is an integrated development environment for theories, proofs, and mathematical tools in Isabelle/ML (based on Poly/ML). System programming is done in Isabelle/Scala.


Platform: Linux, Windows, macOS

Poly/ML version: bundled

Licence: BSD and others

Download link:

Project link: