It is possible to use directly in a ``terminal''. But this is far from the best you can do. You can use the emacs mode developped by C. Raffalli and P. Roziere using D. Aspinall's ``Proof-General''.
This interface works better with XEmacs 21.1 or later, but pre-releases 3.4 of Proof-General works reasonably well with gnu-emacs 21.
You should also note that all it can be used under Windows (98 and XP have been successfully tested), using the win32 version of XEmacs and the specific windows version of .
Proof-General is available from
XEmacs (for Windows and Unix/Linux) is available from