(4steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hzero def
  equal(0,abs_num(zero_rep))
By: HN THEN StrongAuto

Generated subgoal:

1   0 = abs_num(zero_rep)  hnum
3 steps

About:
assertnatural_numberapplyequal
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(4steps total) PrintForm Definitions Lemmas hol num Sections HOLlib Doc