(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 1
  0 = abs_num(zero_rep)  hnum
By: Inst
Thm* 'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'a, r:'b.
Thm* iso_pair('a;'b;P;rep;abs)  rep(a) = r  a = abs(r)
[;;is_num_rep;rep_num;abs_num]
THEN
StrongAuto
THEN
BackThru 1
THEN
StrongAuto

Generated subgoals:

1 1. a,r:.
1. iso_pair(;;is_num_rep;rep_num;abs_num)
1. 
1. rep_num(a) = r    a = abs_num(r)  
  iso_pair(;;is_num_rep;rep_num;abs_num)
1 step
2 1. a,r:.
1. iso_pair(;;is_num_rep;rep_num;abs_num)
1. 
1. rep_num(a) = r    a = abs_num(r)  
  rep_num(0) = zero_rep  
1 step

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

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