Def P  Q == P+Q

is mentioned by

Thm* m,n:. m<n+1  m = n  m<n	[less_thm]
Thm* m,n:. m = n  m<n  m<n+1	[less_lemma2]
Thm* m,n:. m<n+1  m = n  m<n	[less_lemma1]

In prior sections: core bool 1 hol

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