hol
one
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
exists(
rep
:hone
hbool. type_definition((
b
:hbool.
b
),
rep
))
[hone_ty_def]
cites the following:
Thm*
a
:Unit.
a
=
[unit_triviality]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
one
Sections
HOLlib
Doc
rep:hone 
hbool. type_definition((b:hbool. b),rep))
a:Unit. a = 
rep:hone hbool. type_definition((b:hbool. b),rep))a:Unit. a =