Def P  Q == P+Q

is mentioned by

Thm* m,n:. nnsub(m;n) = m  m = 0    n = 0	[sub_eq_eq_0]
Thm* n,m:. n<m  (x:. n = x+m  )	[less_or_eq_add]
Thm* m,n:. m<n  nm	[less_cases]
Thm* m:. 0 = m    0<m	[less_0_cases]

In prior sections: core bool 1 hol hol prim rec int 2 hol arithmetic 3

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