Mention M-h m as keybinding for print_match in interaction guide

Minor tweaking of spacing

Mention existence of menu entries for HOL commands

Update HOL interaction guide

Fix quotes in the HOL4/emacs interaction guide

HOL4 was not recognising Latex curly quotes, so I changed them into
the usual quotes. One can now just copy paste the code into emacs.

I also fixed a typo in the proof of LESS_EQ_MULT.

Tweak some Interaction guide text

Including:
- prefer qexists_tac to Q.EXISTS_TAC, and rpt strip_tac to REPEAT
STRIP_TAC
- mention possibility of Induct_on `term`

Still to do:
- recommend simp, fs, and rfs rather than the current discussion of
using std_ss. bool_ss etc
- maybe mention suffices_by

Update some Interaction comments about doing things in emacs

Specifically:
- .emacs is not the standard place for initialisation anymore
- text-selection can be done by "modern-style" shift-movement of the
cursor

Remove Interaction's claim that hol-mode works with xemacs

Having just tried it, I know it doesn't.

Make Interaction guide's .tex source font-lock better in emacs

Update interaction guide: SML auto-indent

Correct HOL interaction guide: M-h 3 (not C-h 3)

URL tweaks: https

Updates to Interaction guide for release

E.g.:
- update a URL
- prefer lcsymtacs versions of tactics (as per #275)

HOL interaction guide updated

HOL interaction guide updated

do not include extra LaTeX packages

Typo fixed + minor tweaks.

Typo fixed. Thanks to Thomas for spotting the typo.

Fixed a few typos and turned ". " to "{.}~" in places where
LaTeX should not treat . as the end of a sentence.

Minor changes and typo fixes for interaction manual (prefer Once to
ONCE_REWRITE_TAC, mention M-h M-s emacs binding, for example), and
prompted by mention of Once, update various related see-also
references in the documentation.

LaTeX sources for a guide to HOL interaction and
basic proofs (intended for complete beginners).