Def P & Q == PQ

is mentioned by

Thm* x,n,m:. xn & xm  (nnsub(n;x) = nnsub(m;x)  n = m)	[cancel_sub]
Thm* x,n,m:. nx & mx  (nnsub(x;n) = nnsub(x;m)  n = m)	[sub_cancel]
Thm* n,k,r:. (q:. k = qn+r   & r<n)  nmod(k;n) = r	[mod_unique]
Thm* n,k,q:. (r:. k = qn+r   & r<n)  ndiv(k;n) = q	[ndiv_unique]
Thm* k,n:. 0<n  (r,q:. k = qn+r   & r<n)	[da]
Thm* P:(). P(0) & (n:. (m:. m<n  P(m))  P(n))  (n:. P(n))	[gen_induction]
Thm* P:(). (n:. P(n))  (n:. P(n) & (m:. m<n  P(m)))	[wop]
Thm* n,m:. nm & mn  n = m	[less_equal_antisym]
Thm* m,n,x,q:. mx & nq  m+nx+q	[less_eq_less_eq_mono]
Thm* m,n,x:. mn & nx  mx	[less_eq_trans]
Thm* m,n:. 0<m & 0<n  (pre(m) = pre(n)  m = n)	[inv_pre_eq]
Thm* m,n:. m+n = 0    m = 0   & n = 0	[add_eq_0]
Thm* m,n:. Thm* 0m = 0   Thm* & m0 = 0   Thm* & 1m = m   Thm* & m1 = m   Thm* & (m+1)n = mn+n   Thm* & m(n+1) = m+mn	[mult_clauses]
Thm* m,n:. (m<n & nm)	[less_eq_antisym]
Thm* m,n:. m<n & m = n  n<m	[less_cases_imp]
Thm* m,n:. m<n & n = m+1    m+1<n	[less_not_suc]
Thm* m,n:. m<n & m+1 = n    m+1<n	[less_suc_eq_cor]
Thm* 'a:S, f:('a), x1,x2:'a. f(x1) & f(x2)  x1 = x2	[fun_eq_lemma]
Thm* m,n:. (m<n & n<m+1)	[less_less_suc]
Thm* m,n:. (m<n & n<m)	[less_antisym]
Thm* m,n,x:. m<n & n<x  m<x	[less_trans]
Thm* m:. nnsub(0;m) = 0 & nnsub(m;0) = m	[sub_0]

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

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