Def P  Q == P+Q

is mentioned by

Thm* m,n,x:. nnsub(m;n) = x  m = n+x    mn & x0	[sub_right_eq]
Thm* m,n,x:. m = nnsub(n;x)  m+x = n    m0 & nx	[sub_left_eq]
Thm* m,n,x:. xnnsub(m;n)  n+xm  x0	[sub_right_greater_eq]
Thm* m,n,x:. mnnsub(n;x)  m+xn  m0	[sub_left_less_eq]
Thm* m,n:. m = n  m+1n  n+1m	[not_num_eq]
Thm* m,n:. even(mn)  even(m)  even(n)	[even_mult]
Thm* n:. even(n)  odd(n)	[even_or_odd]
Thm* m,n:. mn = 0    m = 0    n = 0	[mult_eq_0]
Thm* m,n:. mn  nm	[less_eq_cases]
Thm* m,n:. m = n  m<n  n<m	[less_less_cases]
Thm* n:. m:. n = (0+1+1)m    n = (0+1+1)m+1	[odd_or_even]

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

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