(46steps total) PrintForm Definitions hol num Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso 1
1. r : 
  abs_num(r) = (@a:. (r = rep_num(a)  ))
By: Unab [`habs_num`] THEN Simp THEN StrongAuto THEN Unfold `hnum` 0

Generated subgoals:

None

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

(46steps total) PrintForm Definitions hol num Sections HOLlib Doc