To run Athena, simply type "athena" at a DOS prompt
at your athena directory (or click "athena.bat" from
Windows Explorer). This will give you an SML-NJ prompt:

       val it = true: bool
       -

At that prompt, type "t();" and press return. That will
give you the top-level Athena prompt ">". You are now
ready to enter and evaluate Athena expressions and deductions.
If you ever get bumped off the Athena prompt and back into
the SML prompt, simply type "t();" again to resume. You may
ignore the "Redefinition" erros you might get once you resume.


Note: You can save your Athena code in a file and then
load the file into Athena by saying ">(load-file file-name)"

Also, you can define things at the top level with the
"define" primitive. E.g. (define x 23.3)

The assumption base is persistent. Theorems established at the
top level are retained in the sequel. 

-----------------------------------------------------------------

If you have any questions, email Kostas Arkoudas at
koud@ai.mit.edu                                                               