Origin Definitions Sections NuprlLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
HOLlib
Nuprl Section: HOLlib - Doug Howe's HOL library.

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.

hol one
hol arithmetic 5
hol arithmetic 4
hol arithmetic 3
hol arithmetic 2
hol list 2
hol list 1
hol restr binder
hol arithmetic 1
hol prim rec
hol pair
hol num
hol sum
hol combin
hol bool
hol min
hol

more to come IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Origin Definitions Sections NuprlLIB Search Doc