Footnotes

Footnotes

 (1)

The only major exception is the functionality of the "Abort" button .

 (2)

The output field displays a plain text description of the state.

 (3)

By clicking on the link "with types", one may investigate the types of the constants.

 (4)

If there is just a single goal, this goal has to be implied. If there is no goal at all, the formula "false" has to be implied (which corresponds to a proof by contradiction).

 (5)

If the template has multiple occurrences of [], pressing the "Tab" key moves the cursor to the next occurrence.

 (6)

The following screenshots of proof states were taken from the already completed proof; the proof state headers listing the applied proof commands and the links to the generated child states are initially not visible.

 (7)

The reader may try the alternative path which leads to a slightly different but essentially equivalent proof.

 (8)

The only exception is the "Abort" button whose effect cannot be achieved by any textual command.

Footnotes