Controlling Isabelle execution

Isabelle prover normally works asynchronously in the background. When you modify the theory file in the editor or just scroll around, the file contents are automatically submitted to the prover (refer to the editor documentation).

Cancel current execution

The current execution of Isabelle prover can be cancelled (stopped) by selecting Isabelle > Cancel Execution in the main menu.

The execution will be resumed if you scroll in the editor, open a new theory file or select Check Active Editor in the menu.

Check all editor contents

A full check of the currently open theory editor can be invoked by selecting Isabelle > Check Active Editor in the main menu.