This is part of Doug Howe's HOL library which is being incrementally mounted (January-February 2004).
It modifies the Nuprl logic to make HOL interpretable.
This translation is based upon Howe's Importing Mathematics from HOL into Nuprl.
more
to
come
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html