From Nuprl the user can request that ML be run interactively by entering the command ml in the command window. Nuprl will respond with a M>
prompt in the command window. Any input typed after this prompt is
processed by ML. This facility allows for the examination of variables
and constants in ML and for the tracing, definition and debugging of
tactics. The user leaves the interactive ML mode by typing 
.
Although definitions can be entered interactively using this mode, the definitions entered are only temporary. Once the current Nuprl session has been concluded, any changes to the ML state disappear. If more permanent definitions are desired an ML object can be created and edited using the text--editing facilities of , and the ML commands in this ML
object can be evaluated by ML. To do this a library object of type ``ML'' is created and then edited in . Once complete this ML object can be checked , during which process the commands of the ML object are evaluated sequentially by ML. If there are no errors in the object it is marked as good, and any changes in the ML state implicit in the commands will remain in effect throughout the remainder of the Nuprl session. Should an error be encountered while evaluating the ML object an error message will be displayed, and evaluation of the ML object will be discontinued. Any error--free commands that preceded the one with an error will have been evaluated with any changes in state remaining in effect. The user may then view the ML object, make the necessary corrections and recheck it. The commands in an ML object will also be evaluated when it is loaded or restored to the library.