Also see the ML Manual for Nuprl4.
This section gives a brief summary of the features of ML. For a complete account the reader is referred to the book Edinburgh LCF [Gordon, Milner, & Wadsworth 79]. Originally, ML was developed as the metalanguage for the LCF proof system; several dialects of the language have since evolved, including Cambridge ML, the implementation of ML used in Nuprl . The ML used in Nuprl differs in several minor ways from the original ML, for we have specialized the language to the Nuprl logic.
The principal features of ML are: