IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The ML programming language of Nuprl
Executable code for Tactics (as well as a lot of editor code) is written in a dialect of ML described in the
ML manual (postscript).
It is older than Standard ML. The term "ML" connotes the fact that it was a "meta-language" of computation for an earlier tactic prover at Edinburgh, namely LCF, as it is now for Nuprl. Some new primitive types, including "term" and "proof", were added.