Isamode Using Isabelle with XEmacs Home News Download Documentation Links

Isamode is a front-end for the theorem prover Isabelle.

It provides many useful features including an editing mode for theory files, and an Isabelle interaction mode which provides multiple windows and pull down menus. The multiple windows are used to separately display the proof state, the Isabelle shell, and the current theory.

Isamode is tightly integrated with the XEmacs editor.

Isamode was actively developed from 1994 until 1998. Since then it has not been developed, but maintenance releases have been made to keep things working with newer versions of Isabelle and XEmacs. Instead of developing Isamode further, I have worked on Proof General, a generic front-end for several proof assistants, including Isabelle.