Revised TUTORIAL for HOL-Omega.

This is the long-awaited HOL-Omega tutorial, realized as an expansion
of the existing HOL tutorial, with several new chapters added.