The Nuprl book Implementing Mathematics with the Nuprl Proof Development System, Constable et al, published in 1986, is still a good background reference. However, the system has changed sufficiently that none of the tutorials given in the book will work in the current system. The ``reference'' portion, excluding the parts of Chapter 8 on the type system and its semantics, is superseded by this reference manual. Chapter 9 in the reference portion also contains some useful examples and discussions of tactic writing that are not reproduced here. The ``advanced'' portion of the book deals with application methodology, gives some extended examples of mathematics formalized in Nuprl, and also describes some extensions to the type theory which have not been implemented.
Substantial changes have been made to Nuprl since the book was written. The most major ones are: