The current system is the FDL.
    Nuprl 4 is also still available (see below).
FDL
Nuprl 5 has been subsumed by the FDL (Formal Digital Library).
Nuprl5 survives as a refiner the FDL can use to verify and produce formal content.
Most Nuprl5 editor and library features have been included in the FDL.
The FDL is available via anonymous ftp from ftp.cs.cornell.edu.
cd pub/nuprl/fdl
get README.ftp
Then follow the instructions in README.ftp
The nuprl5 User Documentation still applies to the FDL:
The Nuprl WWW browser has been updated to contain those
theories released with Nuprl 4.2. There are a number of new Algebra theories.
We have a patch for some omissions in the standard CLX
distribution relating to Lucid Common Lisp. See the lucid-clx-patch directory
at the aforementioned nuprl4 ftp site.