(46steps total) PrintForm Definitions hol num Sections HOLlib Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: num iso
  iso_pair(;;is_num_rep;rep_num;abs_num)
By: Unab [`iso_pair`;`type_definition`] THEN Simp THEN StrongAuto
THEN
Try (Complete (Unfold `hnum` 0))

Generated subgoals:

1 1. r : 
  abs_num(r) = (@a:. (r = rep_num(a)  ))
1 step
2 1. x' : 
2. x'' : 
3. rep_num(x') = rep_num(x'')  
  x' = x''
27 steps
3 1. x : 
2. is_num_rep(x)
  x':. x = rep_num(x')  
7 steps
4 1. x : 
2. x':. x = rep_num(x')  
  is_num_rep(x)
10 steps

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

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