Def type_definition == P:'a. rep:'b'a. type_definition('a;'b;P;rep)

is mentioned by

Thm* 'b,'a:S. Thm* all Thm* (P:'a  hbool. all Thm* (P:'a  hbool. (rep:'b  'a. equal Thm* (P:'a  hbool. (rep:'b  'a. (type_definition(P,rep) Thm* (P:'a  hbool. (rep:'b  'a. ,and Thm* (P:'a  hbool. (rep:'b  'a. ,(all Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. all Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. implies Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. (equal Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. ((rep(x') Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. (,rep(x'')) Thm* (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. ,equal(x',x'')))) Thm* (P:'a  hbool. (rep:'b  'a. ,,all Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. equal Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. (P(x) Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,exists Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. equal Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. (x Thm* (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. ,rep(x')))))))))

[htype_definition_wd]

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