is mentioned by

Thm* 'a,'b:S, p:('a'b). p = <1of(p),2of(p)>	[pair_unfold]
Thm* 'a,'b:S, x:('a'b). <1of(x),2of(x)> = x	[pair_wd]
Def uncurry == f:'a'b'c. p:'a'b. f(1of(p),2of(p))	[huncurry]
Def fst == p:'a'b. 1of(p)	[hfst]
Def rep_prod == p:'a'b. mk_pair(1of(p),2of(p))	[hrep_prod]

In prior sections: core hol

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html