When you have written a file foo.phx, you can compile it using the command:
phox -c foo.phx
This compilation generates two files foo.phi and foo.pho and
possibly one or more LaTeX file (see the chapter 9).
The file foo.pho is a core image of just after the
compilation. You can use it to restart in a state equivalent to the
state it had after reading the last line of the file foo.phx. This is
useful when developing to avoid executing each line in the file before
continuing it.
The file foo.phi is used when you want to reuse the theory developed in
the file foo.phx. To do so you can use the command:
Import foo.
This command includes all the objects declared in the file foo.phx. The
above rules are used to resolve name conflicts.