# Footnotes

### (1)

A *proof assistant* is a computerized helper for
developing mathematical proofs. For short, we sometimes call it a
*prover*, although we always have in mind an interactive system
rather than a fully automated theorem prover.

### (2)

A *proof script* is a sequence of commands
which constructs a proof, usually stored in a file.

### (3)

Some proof assistants provide some level of support for switching between multiple concurrent proofs, but Proof General does not use this. Generally the exact context for such proofs is hard to define to easily split them into multiple files.

### (4)

In fact, this is an unnecessary restriction imposed by the original design of Proof General. There is nothing to stop future versions of Proof General allowing the queue region to be extended or shrunk, whilst the prover is processing it. Proof General 3.0 already relaxes the original design, by allowing successive assertion commands without complaining.

### (5)

The suffix may depend of
the specific proof assistant you are using e.g, LEGO’s proof script
files have to end with ‘`.l`’.

### (6)

For example, LEGO generates additional compiled (optimised) proof script files for efficiency.

### (7)

And please, don’t even think of including those in your LEGO proof script!

This document was generated by *Erik Martin-Dorel* on *June 2, 2019* using *texi2html 1.82*.