When compiling a file (using the phox -c command) you can
generate one or more LaTeX documents. This generation is NOT automatic. But
can produce a LaTeX version of any formula available in the current
context. This means that when you want to present your proof informally, you
can insert easily the current goal or hypothesis in your document. In practice
you almost never need to write mathematical formulas in LaTeX yourself. When
a formula does not fit on one line, you can tell to break it
automatically for you (this will require two compilations in LaTeX and the
use of a small external tool pretty to decide where to break).
You can also specify the LaTeX syntax of any constant or definition so that they look like you wish. In fact using all these possibilities, you can completely hide the fact that your paper comes from a machine assisted proof !
The LaTeX file produced by can be used as stand-alone articles or inserted in a bigger document (which can be partially written in pure LaTeX).
In this chapter, we assume that the reader as a basic knowledge of LaTeX.