Def P  Q == PQ

is mentioned by

Thm* n:. (even(n)  (m:. n = 2m  )) & (odd(n)  (m:. n = 2m+1  ))	[even_odd_exists]
Thm* m,n,x:. m<n & nx  m<x	[less_less_eq_trans]
Thm* m,n,x:. mn & n<x  m<x	[less_eq_less_trans]
Thm* m,n:. 0<m & 0<n  0<mn	[less_mult2]
Thm* m,n:. mn  (x:. n = m+x  )	[less_equal_add]

In prior sections: core fun 1 well fnd int 1 bool 1 hol hol bool hol num hol prim rec hol arithmetic 1 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