Download

Naproche is distributed as part of Isabelle, with downloads available for Windows, macOS, and Linux. Naproche uses Isabelle’s integrated development environment and its bundled automated provers, but is unconnected to Isabelle’s logics.

On macOS, when first opening Isabelle, you may need to control-click the .app bundle and select “Open” to bypass Apple’s Gatekeeper. You will find a short introduction to Naproche in the Examples section of the Documentation panel on the left of the IDE. Opening a ForTheL file in ASCII format (.ftl) or LaTeX format (.ftl.tex) in the Isabelle/jEdit editor will automatically invoke its continuous checking by Naproche.

Naproche is open source and its source code is freely available on GitHub.