Nuprl - hol_num LEMMAs for induction

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

Theorem	Name
Thm* P:(). P(0) & (n:. P(n) P(n+1)) (n:. P(n))	[induction]
cites the following:
Thm* all Thm* (P:hnum hbool. implies Thm* (P:hnum hbool. (and(P(0),all(n:hnum. implies(P(n),P(suc(n))))) Thm* (P:hnum hbool. ,all(n:hnum. P(n))))	[hinduction]

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