NuprlLib
Doc
Pavel Naumov
conceived and originated the projection of the
Nuprl Math Library
onto the web by means of html. Had he not done that, we might still be waiting to get around to "publishing" our library.
See his
"Publishing Formal Mathematics on the Web" (postscript)
.
(Oct 2001 -
sfa
)
NuprlLib
Doc