'a:S. all(
e:'a. exists_unique(fn:hone 
'a. equal(fn(one_el),e)))v:hone. equal(v,one_el))'a:S. all(f:'a hone. all(g:'a hone. equal(f,g)))x:hone. t))rep:hone hbool. type_definition((b:hbool. b),rep))is mentioned by
| 'a:S. all(e:'a. exists_unique(fn:hone 'a. equal(fn(one_el),e))) | [hone_axiom_2] |
| v:hone. equal(v,one_el)) | [hone_wd] |
| 'a:S. all(f:'a hone. all(g:'a hone. equal(f,g))) | [hone_axiom] |
| x:hone. t)) | [hone_def] |
| rep:hone hbool. type_definition((b:hbool. b),rep)) | [hone_ty_def] |
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html