Getting started.

To start , you only need to open with XEmacs a file whose name ends by the extension .phx. Try it, you should see a screen similar to the figure 2.1.

Figure: Sample of a screen under XEmacs with Proof-General

When using the interface, you use two ``buffers'' (division of a window where XEmacs displays text). One buffer represents your file. The other contains the answer from the system.

You should remark that under XEmacs (not Emacs) some symbols are displayed with a nice mathematical syntax. Moreover, when the mouse pointer moves above such symbol, you can see there ASCII equivalent.

To use it, you simply type in the file and transmit command to the system using the navigation buttons. The command that have been transmitted are highlighted with a different background color and are locked (you can not edit them anymore). The main navigation button are:

Next

sends the next command to the system.

Undo

go back from one command.

Goto

enter (or undo) all the commands to move to a specific position in the file.

Restart

restart (sometimes very useful, because synchronisation between the system and XEmacs is lost. In this case you to Restart followed by Goto.

All these buttons are also associated to a menu and a keyboard equivalent (visible in the menu).